# HG changeset patch
# User wenzelm
# Date 1412708491 -7200
# Node ID c38d8f139bbcc4302949cbf785f21ff981a0ed34
# Parent  5b7f0b5da8848553550d156d7b1a30faf5058f03# Parent  7338eb25226c3a06a9d9cf1066326918e4db71c4
merged

diff -r 7338eb25226c -r c38d8f139bbc src/HOL/Datatype_Examples/Koenig.thy
--- a/src/HOL/Datatype_Examples/Koenig.thy	Tue Oct 07 20:59:46 2014 +0200
+++ b/src/HOL/Datatype_Examples/Koenig.thy	Tue Oct 07 21:01:31 2014 +0200
@@ -9,7 +9,7 @@
 header {* Koenig's Lemma *}
 
 theory Koenig
-imports TreeFI Stream
+imports TreeFI "~~/src/HOL/Library/Stream"
 begin
 
 (* infinite trees: *)
diff -r 7338eb25226c -r c38d8f139bbc src/HOL/Datatype_Examples/Process.thy
--- a/src/HOL/Datatype_Examples/Process.thy	Tue Oct 07 20:59:46 2014 +0200
+++ b/src/HOL/Datatype_Examples/Process.thy	Tue Oct 07 21:01:31 2014 +0200
@@ -8,7 +8,7 @@
 header {* Processes *}
 
 theory Process
-imports Stream 
+imports "~~/src/HOL/Library/Stream"
 begin
 
 codatatype 'a process =
diff -r 7338eb25226c -r c38d8f139bbc src/HOL/Datatype_Examples/Stream.thy
--- a/src/HOL/Datatype_Examples/Stream.thy	Tue Oct 07 20:59:46 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,582 +0,0 @@
-(*  Title:      HOL/Datatype_Examples/Stream.thy
-    Author:     Dmitriy Traytel, TU Muenchen
-    Author:     Andrei Popescu, TU Muenchen
-    Copyright   2012, 2013
-
-Infinite streams.
-*)
-
-header {* Infinite Streams *}
-
-theory Stream
-imports "~~/src/HOL/Library/Nat_Bijection"
-begin
-
-codatatype (sset: 'a) stream =
-  SCons (shd: 'a) (stl: "'a stream") (infixr "##" 65)
-for
-  map: smap
-  rel: stream_all2
-
-(*for code generation only*)
-definition smember :: "'a \<Rightarrow> 'a stream \<Rightarrow> bool" where
-  [code_abbrev]: "smember x s \<longleftrightarrow> x \<in> sset s"
-
-lemma smember_code[code, simp]: "smember x (y ## s) = (if x = y then True else smember x s)"
-  unfolding smember_def by auto
-
-hide_const (open) smember
-
-lemmas smap_simps[simp] = stream.map_sel
-lemmas shd_sset = stream.set_sel(1)
-lemmas stl_sset = stream.set_sel(2)
-
-theorem sset_induct[consumes 1, case_names shd stl, induct set: sset]:
-  assumes "y \<in> sset s" and "\<And>s. P (shd s) s" and "\<And>s y. \<lbrakk>y \<in> sset (stl s); P y (stl s)\<rbrakk> \<Longrightarrow> P y s"
-  shows "P y s"
-using assms by induct (metis stream.sel(1), auto)
-
-
-subsection {* prepend list to stream *}
-
-primrec shift :: "'a list \<Rightarrow> 'a stream \<Rightarrow> 'a stream" (infixr "@-" 65) where
-  "shift [] s = s"
-| "shift (x # xs) s = x ## shift xs s"
-
-lemma smap_shift[simp]: "smap f (xs @- s) = map f xs @- smap f s"
-  by (induct xs) auto
-
-lemma shift_append[simp]: "(xs @ ys) @- s = xs @- ys @- s"
-  by (induct xs) auto
-
-lemma shift_simps[simp]:
-   "shd (xs @- s) = (if xs = [] then shd s else hd xs)"
-   "stl (xs @- s) = (if xs = [] then stl s else tl xs @- s)"
-  by (induct xs) auto
-
-lemma sset_shift[simp]: "sset (xs @- s) = set xs \<union> sset s"
-  by (induct xs) auto
-
-lemma shift_left_inj[simp]: "xs @- s1 = xs @- s2 \<longleftrightarrow> s1 = s2"
-  by (induct xs) auto
-
-
-subsection {* set of streams with elements in some fixed set *}
-
-coinductive_set
-  streams :: "'a set \<Rightarrow> 'a stream set"
-  for A :: "'a set"
-where
-  Stream[intro!, simp, no_atp]: "\<lbrakk>a \<in> A; s \<in> streams A\<rbrakk> \<Longrightarrow> a ## s \<in> streams A"
-
-lemma shift_streams: "\<lbrakk>w \<in> lists A; s \<in> streams A\<rbrakk> \<Longrightarrow> w @- s \<in> streams A"
-  by (induct w) auto
-
-lemma streams_Stream: "x ## s \<in> streams A \<longleftrightarrow> x \<in> A \<and> s \<in> streams A"
-  by (auto elim: streams.cases)
-
-lemma streams_stl: "s \<in> streams A \<Longrightarrow> stl s \<in> streams A"
-  by (cases s) (auto simp: streams_Stream)
-
-lemma streams_shd: "s \<in> streams A \<Longrightarrow> shd s \<in> A"
-  by (cases s) (auto simp: streams_Stream)
-
-lemma sset_streams:
-  assumes "sset s \<subseteq> A"
-  shows "s \<in> streams A"
-using assms proof (coinduction arbitrary: s)
-  case streams then show ?case by (cases s) simp
-qed
-
-lemma streams_sset:
-  assumes "s \<in> streams A"
-  shows "sset s \<subseteq> A"
-proof
-  fix x assume "x \<in> sset s" from this `s \<in> streams A` show "x \<in> A"
-    by (induct s) (auto intro: streams_shd streams_stl)
-qed
-
-lemma streams_iff_sset: "s \<in> streams A \<longleftrightarrow> sset s \<subseteq> A"
-  by (metis sset_streams streams_sset)
-
-lemma streams_mono:  "s \<in> streams A \<Longrightarrow> A \<subseteq> B \<Longrightarrow> s \<in> streams B"
-  unfolding streams_iff_sset by auto
-
-lemma smap_streams: "s \<in> streams A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<in> B) \<Longrightarrow> smap f s \<in> streams B"
-  unfolding streams_iff_sset stream.set_map by auto
-
-lemma streams_empty: "streams {} = {}"
-  by (auto elim: streams.cases)
-
-lemma streams_UNIV[simp]: "streams UNIV = UNIV"
-  by (auto simp: streams_iff_sset)
-
-subsection {* nth, take, drop for streams *}
-
-primrec snth :: "'a stream \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
-  "s !! 0 = shd s"
-| "s !! Suc n = stl s !! n"
-
-lemma snth_smap[simp]: "smap f s !! n = f (s !! n)"
-  by (induct n arbitrary: s) auto
-
-lemma shift_snth_less[simp]: "p < length xs \<Longrightarrow> (xs @- s) !! p = xs ! p"
-  by (induct p arbitrary: xs) (auto simp: hd_conv_nth nth_tl)
-
-lemma shift_snth_ge[simp]: "p \<ge> length xs \<Longrightarrow> (xs @- s) !! p = s !! (p - length xs)"
-  by (induct p arbitrary: xs) (auto simp: Suc_diff_eq_diff_pred)
-
-lemma shift_snth: "(xs @- s) !! n = (if n < length xs then xs ! n else s !! (n - length xs))"
-  by auto
-
-lemma snth_sset[simp]: "s !! n \<in> sset s"
-  by (induct n arbitrary: s) (auto intro: shd_sset stl_sset)
-
-lemma sset_range: "sset s = range (snth s)"
-proof (intro equalityI subsetI)
-  fix x assume "x \<in> sset s"
-  thus "x \<in> range (snth s)"
-  proof (induct s)
-    case (stl s x)
-    then obtain n where "x = stl s !! n" by auto
-    thus ?case by (auto intro: range_eqI[of _ _ "Suc n"])
-  qed (auto intro: range_eqI[of _ _ 0])
-qed auto
-
-primrec stake :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a list" where
-  "stake 0 s = []"
-| "stake (Suc n) s = shd s # stake n (stl s)"
-
-lemma length_stake[simp]: "length (stake n s) = n"
-  by (induct n arbitrary: s) auto
-
-lemma stake_smap[simp]: "stake n (smap f s) = map f (stake n s)"
-  by (induct n arbitrary: s) auto
-
-lemma take_stake: "take n (stake m s) = stake (min n m) s"
-proof (induct m arbitrary: s n)
-  case (Suc m) thus ?case by (cases n) auto
-qed simp
-
-primrec sdrop :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where
-  "sdrop 0 s = s"
-| "sdrop (Suc n) s = sdrop n (stl s)"
-
-lemma sdrop_simps[simp]:
-  "shd (sdrop n s) = s !! n" "stl (sdrop n s) = sdrop (Suc n) s"
-  by (induct n arbitrary: s)  auto
-
-lemma sdrop_smap[simp]: "sdrop n (smap f s) = smap f (sdrop n s)"
-  by (induct n arbitrary: s) auto
-
-lemma sdrop_stl: "sdrop n (stl s) = stl (sdrop n s)"
-  by (induct n) auto
-
-lemma drop_stake: "drop n (stake m s) = stake (m - n) (sdrop n s)"
-proof (induct m arbitrary: s n)
-  case (Suc m) thus ?case by (cases n) auto
-qed simp
-
-lemma stake_sdrop: "stake n s @- sdrop n s = s"
-  by (induct n arbitrary: s) auto
-
-lemma id_stake_snth_sdrop:
-  "s = stake i s @- s !! i ## sdrop (Suc i) s"
-  by (subst stake_sdrop[symmetric, of _ i]) (metis sdrop_simps stream.collapse)
-
-lemma smap_alt: "smap f s = s' \<longleftrightarrow> (\<forall>n. f (s !! n) = s' !! n)" (is "?L = ?R")
-proof
-  assume ?R
-  then have "\<And>n. smap f (sdrop n s) = sdrop n s'"
-    by coinduction (auto intro: exI[of _ 0] simp del: sdrop.simps(2))
-  then show ?L using sdrop.simps(1) by metis
-qed auto
-
-lemma stake_invert_Nil[iff]: "stake n s = [] \<longleftrightarrow> n = 0"
-  by (induct n) auto
-
-lemma sdrop_shift: "sdrop i (w @- s) = drop i w @- sdrop (i - length w) s"
-  by (induct i arbitrary: w s) (auto simp: drop_tl drop_Suc neq_Nil_conv)
-
-lemma stake_shift: "stake i (w @- s) = take i w @ stake (i - length w) s"
-  by (induct i arbitrary: w s) (auto simp: neq_Nil_conv)
-
-lemma stake_add[simp]: "stake m s @ stake n (sdrop m s) = stake (m + n) s"
-  by (induct m arbitrary: s) auto
-
-lemma sdrop_add[simp]: "sdrop n (sdrop m s) = sdrop (m + n) s"
-  by (induct m arbitrary: s) auto
-
-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 
-  "sdrop_while P s = (if P (shd s) then sdrop_while P (stl s) else s)"
-
-lemma sdrop_while_SCons[code]:
-  "sdrop_while P (a ## s) = (if P a then sdrop_while P s else a ## s)"
-  by (subst sdrop_while.simps) simp
-
-lemma sdrop_while_sdrop_LEAST:
-  assumes "\<exists>n. P (s !! n)"
-  shows "sdrop_while (Not o P) s = sdrop (LEAST n. P (s !! n)) s"
-proof -
-  from assms obtain m where "P (s !! m)" "\<And>n. P (s !! n) \<Longrightarrow> m \<le> n"
-    and *: "(LEAST n. P (s !! n)) = m" by atomize_elim (auto intro: LeastI Least_le)
-  thus ?thesis unfolding *
-  proof (induct m arbitrary: s)
-    case (Suc m)
-    hence "sdrop_while (Not \<circ> P) (stl s) = sdrop m (stl s)"
-      by (metis (full_types) not_less_eq_eq snth.simps(2))
-    moreover from Suc(3) have "\<not> (P (s !! 0))" by blast
-    ultimately show ?case by (subst sdrop_while.simps) simp
-  qed (metis comp_apply sdrop.simps(1) sdrop_while.simps snth.simps(1))
-qed
-
-primcorec sfilter where
-  "shd (sfilter P s) = shd (sdrop_while (Not o P) s)"
-| "stl (sfilter P s) = sfilter P (stl (sdrop_while (Not o P) s))"
-
-lemma sfilter_Stream: "sfilter P (x ## s) = (if P x then x ## sfilter P s else sfilter P s)"
-proof (cases "P x")
-  case True thus ?thesis by (subst sfilter.ctr) (simp add: sdrop_while_SCons)
-next
-  case False thus ?thesis by (subst (1 2) sfilter.ctr) (simp add: sdrop_while_SCons)
-qed
-
-
-subsection {* unary predicates lifted to streams *}
-
-definition "stream_all P s = (\<forall>p. P (s !! p))"
-
-lemma stream_all_iff[iff]: "stream_all P s \<longleftrightarrow> Ball (sset s) P"
-  unfolding stream_all_def sset_range by auto
-
-lemma stream_all_shift[simp]: "stream_all P (xs @- s) = (list_all P xs \<and> stream_all P s)"
-  unfolding stream_all_iff list_all_iff by auto
-
-lemma stream_all_Stream: "stream_all P (x ## X) \<longleftrightarrow> P x \<and> stream_all P X"
-  by simp
-
-
-subsection {* recurring stream out of a list *}
-
-primcorec cycle :: "'a list \<Rightarrow> 'a stream" where
-  "shd (cycle xs) = hd xs"
-| "stl (cycle xs) = cycle (tl xs @ [hd xs])"
-
-lemma cycle_decomp: "u \<noteq> [] \<Longrightarrow> cycle u = u @- cycle u"
-proof (coinduction arbitrary: u)
-  case Eq_stream then show ?case using stream.collapse[of "cycle u"]
-    by (auto intro!: exI[of _ "tl u @ [hd u]"])
-qed
-
-lemma cycle_Cons[code]: "cycle (x # xs) = x ## cycle (xs @ [x])"
-  by (subst cycle.ctr) simp
-
-lemma cycle_rotated: "\<lbrakk>v \<noteq> []; cycle u = v @- s\<rbrakk> \<Longrightarrow> cycle (tl u @ [hd u]) = tl v @- s"
-  by (auto dest: arg_cong[of _ _ stl])
-
-lemma stake_append: "stake n (u @- s) = take (min (length u) n) u @ stake (n - length u) s"
-proof (induct n arbitrary: u)
-  case (Suc n) thus ?case by (cases u) auto
-qed auto
-
-lemma stake_cycle_le[simp]:
-  assumes "u \<noteq> []" "n < length u"
-  shows "stake n (cycle u) = take n u"
-using min_absorb2[OF less_imp_le_nat[OF assms(2)]]
-  by (subst cycle_decomp[OF assms(1)], subst stake_append) auto
-
-lemma stake_cycle_eq[simp]: "u \<noteq> [] \<Longrightarrow> stake (length u) (cycle u) = u"
-  by (subst cycle_decomp) (auto simp: stake_shift)
-
-lemma sdrop_cycle_eq[simp]: "u \<noteq> [] \<Longrightarrow> sdrop (length u) (cycle u) = cycle u"
-  by (subst cycle_decomp) (auto simp: sdrop_shift)
-
-lemma stake_cycle_eq_mod_0[simp]: "\<lbrakk>u \<noteq> []; n mod length u = 0\<rbrakk> \<Longrightarrow>
-   stake n (cycle u) = concat (replicate (n div length u) u)"
-  by (induct "n div length u" arbitrary: n u) (auto simp: stake_add[symmetric])
-
-lemma sdrop_cycle_eq_mod_0[simp]: "\<lbrakk>u \<noteq> []; n mod length u = 0\<rbrakk> \<Longrightarrow>
-   sdrop n (cycle u) = cycle u"
-  by (induct "n div length u" arbitrary: n u) (auto simp: sdrop_add[symmetric])
-
-lemma stake_cycle: "u \<noteq> [] \<Longrightarrow>
-   stake n (cycle u) = concat (replicate (n div length u) u) @ take (n mod length u) u"
-  by (subst mod_div_equality[of n "length u", symmetric], unfold stake_add[symmetric]) auto
-
-lemma sdrop_cycle: "u \<noteq> [] \<Longrightarrow> sdrop n (cycle u) = cycle (rotate (n mod length u) u)"
-  by (induct n arbitrary: u) (auto simp: rotate1_rotate_swap rotate1_hd_tl rotate_conv_mod[symmetric])
-
-
-subsection {* iterated application of a function *}
-
-primcorec siterate where
-  "shd (siterate f x) = x"
-| "stl (siterate f x) = siterate f (f x)"
-
-lemma stake_Suc: "stake (Suc n) s = stake n s @ [s !! n]"
-  by (induct n arbitrary: s) auto
-
-lemma snth_siterate[simp]: "siterate f x !! n = (f^^n) x"
-  by (induct n arbitrary: x) (auto simp: funpow_swap1)
-
-lemma sdrop_siterate[simp]: "sdrop n (siterate f x) = siterate f ((f^^n) x)"
-  by (induct n arbitrary: x) (auto simp: funpow_swap1)
-
-lemma stake_siterate[simp]: "stake n (siterate f x) = map (\<lambda>n. (f^^n) x) [0 ..< n]"
-  by (induct n arbitrary: x) (auto simp del: stake.simps(2) simp: stake_Suc)
-
-lemma sset_siterate: "sset (siterate f x) = {(f^^n) x | n. True}"
-  by (auto simp: sset_range)
-
-lemma smap_siterate: "smap f (siterate f x) = siterate f (f x)"
-  by (coinduction arbitrary: x) auto
-
-
-subsection {* stream repeating a single element *}
-
-abbreviation "sconst \<equiv> siterate id"
-
-lemma shift_replicate_sconst[simp]: "replicate n x @- sconst x = sconst x"
-  by (subst (3) stake_sdrop[symmetric]) (simp add: map_replicate_trivial)
-
-lemma sset_sconst[simp]: "sset (sconst x) = {x}"
-  by (simp add: sset_siterate)
-
-lemma sconst_alt: "s = sconst x \<longleftrightarrow> sset s = {x}"
-proof
-  assume "sset s = {x}"
-  then show "s = sconst x"
-  proof (coinduction arbitrary: s)
-    case Eq_stream
-    then have "shd s = x" "sset (stl s) \<subseteq> {x}" by (case_tac [!] s) auto
-    then have "sset (stl s) = {x}" by (cases "stl s") auto
-    with `shd s = x` show ?case by auto
-  qed
-qed simp
-
-lemma same_cycle: "sconst x = cycle [x]"
-  by coinduction auto
-
-lemma smap_sconst: "smap f (sconst x) = sconst (f x)"
-  by coinduction auto
-
-lemma sconst_streams: "x \<in> A \<Longrightarrow> sconst x \<in> streams A"
-  by (simp add: streams_iff_sset)
-
-
-subsection {* stream of natural numbers *}
-
-abbreviation "fromN \<equiv> siterate Suc"
-
-abbreviation "nats \<equiv> fromN 0"
-
-lemma sset_fromN[simp]: "sset (fromN n) = {n ..}"
-  by (auto simp add: sset_siterate le_iff_add)
-
-lemma stream_smap_fromN: "s = smap (\<lambda>j. let i = j - n in s !! i) (fromN n)"
-  by (coinduction arbitrary: s n)
-    (force simp: neq_Nil_conv Let_def snth.simps(2)[symmetric] Suc_diff_Suc
-      intro: stream.map_cong split: if_splits simp del: snth.simps(2))
-
-lemma stream_smap_nats: "s = smap (snth s) nats"
-  using stream_smap_fromN[where n = 0] by simp
-
-
-subsection {* flatten a stream of lists *}
-
-primcorec flat where
-  "shd (flat ws) = hd (shd ws)"
-| "stl (flat ws) = flat (if tl (shd ws) = [] then stl ws else tl (shd ws) ## stl ws)"
-
-lemma flat_Cons[simp, code]: "flat ((x # xs) ## ws) = x ## flat (if xs = [] then ws else xs ## ws)"
-  by (subst flat.ctr) simp
-
-lemma flat_Stream[simp]: "xs \<noteq> [] \<Longrightarrow> flat (xs ## ws) = xs @- flat ws"
-  by (induct xs) auto
-
-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 
-  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> 
-  sset (flat s) = (\<Union>xs \<in> sset s. set xs)" (is "?P \<Longrightarrow> ?L = ?R")
-proof safe
-  fix x assume ?P "x : ?L"
-  then obtain m where "x = flat s !! m" by (metis image_iff sset_range)
-  with `?P` obtain n m' where "x = s !! n ! m'" "m' < length (s !! n)"
-  proof (atomize_elim, induct m arbitrary: s rule: less_induct)
-    case (less y)
-    thus ?case
-    proof (cases "y < length (shd s)")
-      case True thus ?thesis by (metis flat_snth less(2,3) snth.simps(1))
-    next
-      case False
-      hence "x = flat (stl s) !! (y - length (shd s))" by (metis less(2,3) flat_snth)
-      moreover
-      { from less(2) have *: "length (shd s) > 0" by (cases s) simp_all
-        with False have "y > 0" by (cases y) simp_all
-        with * have "y - length (shd s) < y" by simp
-      }
-      moreover have "\<forall>xs \<in> sset (stl s). xs \<noteq> []" using less(2) by (cases s) auto
-      ultimately have "\<exists>n m'. x = stl s !! n ! m' \<and> m' < length (stl s !! n)" by (intro less(1)) auto
-      thus ?thesis by (metis snth.simps(2))
-    qed
-  qed
-  thus "x \<in> ?R" by (auto simp: sset_range dest!: nth_mem)
-next
-  fix x xs assume "xs \<in> sset s" ?P "x \<in> set xs" thus "x \<in> ?L"
-    by (induct rule: sset_induct)
-      (metis UnI1 flat_unfold shift.simps(1) sset_shift,
-       metis UnI2 flat_unfold shd_sset stl_sset sset_shift)
-qed
-
-
-subsection {* merge a stream of streams *}
-
-definition smerge :: "'a stream stream \<Rightarrow> 'a stream" where
-  "smerge ss = flat (smap (\<lambda>n. map (\<lambda>s. s !! n) (stake (Suc n) ss) @ stake n (ss !! n)) nats)"
-
-lemma stake_nth[simp]: "m < n \<Longrightarrow> stake n s ! m = s !! m"
-  by (induct n arbitrary: s m) (auto simp: nth_Cons', metis Suc_pred snth.simps(2))
-
-lemma snth_sset_smerge: "ss !! n !! m \<in> sset (smerge ss)"
-proof (cases "n \<le> m")
-  case False thus ?thesis unfolding smerge_def
-    by (subst sset_flat)
-      (auto simp: stream.set_map in_set_conv_nth simp del: stake.simps
-        intro!: exI[of _ n, OF disjI2] exI[of _ m, OF mp])
-next
-  case True thus ?thesis unfolding smerge_def
-    by (subst sset_flat)
-      (auto simp: stream.set_map in_set_conv_nth image_iff simp del: stake.simps snth.simps
-        intro!: exI[of _ m, OF disjI1] bexI[of _ "ss !! n"] exI[of _ n, OF mp])
-qed
-
-lemma sset_smerge: "sset (smerge ss) = UNION (sset ss) sset"
-proof safe
-  fix x assume "x \<in> sset (smerge ss)"
-  thus "x \<in> UNION (sset ss) sset"
-    unfolding smerge_def by (subst (asm) sset_flat)
-      (auto simp: stream.set_map in_set_conv_nth sset_range simp del: stake.simps, fast+)
-next
-  fix s x assume "s \<in> sset ss" "x \<in> sset s"
-  thus "x \<in> sset (smerge ss)" using snth_sset_smerge by (auto simp: sset_range)
-qed
-
-
-subsection {* product of two streams *}
-
-definition sproduct :: "'a stream \<Rightarrow> 'b stream \<Rightarrow> ('a \<times> 'b) stream" where
-  "sproduct s1 s2 = smerge (smap (\<lambda>x. smap (Pair x) s2) s1)"
-
-lemma sset_sproduct: "sset (sproduct s1 s2) = sset s1 \<times> sset s2"
-  unfolding sproduct_def sset_smerge by (auto simp: stream.set_map)
-
-
-subsection {* interleave two streams *}
-
-primcorec sinterleave where
-  "shd (sinterleave s1 s2) = shd s1"
-| "stl (sinterleave s1 s2) = sinterleave s2 (stl s1)"
-
-lemma sinterleave_code[code]:
-  "sinterleave (x ## s1) s2 = x ## sinterleave s2 s1"
-  by (subst sinterleave.ctr) simp
-
-lemma sinterleave_snth[simp]:
-  "even n \<Longrightarrow> sinterleave s1 s2 !! n = s1 !! (n div 2)"
-   "odd n \<Longrightarrow> sinterleave s1 s2 !! n = s2 !! (n div 2)"
-  by (induct n arbitrary: s1 s2)
-    (auto dest: even_nat_Suc_div_2 odd_nat_plus_one_div_two[folded nat_2])
-
-lemma sset_sinterleave: "sset (sinterleave s1 s2) = sset s1 \<union> sset s2"
-proof (intro equalityI subsetI)
-  fix x assume "x \<in> sset (sinterleave s1 s2)"
-  then obtain n where "x = sinterleave s1 s2 !! n" unfolding sset_range by blast
-  thus "x \<in> sset s1 \<union> sset s2" by (cases "even n") auto
-next
-  fix x assume "x \<in> sset s1 \<union> sset s2"
-  thus "x \<in> sset (sinterleave s1 s2)"
-  proof
-    assume "x \<in> sset s1"
-    then obtain n where "x = s1 !! n" unfolding sset_range by blast
-    hence "sinterleave s1 s2 !! (2 * n) = x" by simp
-    thus ?thesis unfolding sset_range by blast
-  next
-    assume "x \<in> sset s2"
-    then obtain n where "x = s2 !! n" unfolding sset_range by blast
-    hence "sinterleave s1 s2 !! (2 * n + 1) = x" by simp
-    thus ?thesis unfolding sset_range by blast
-  qed
-qed
-
-
-subsection {* zip *}
-
-primcorec szip where
-  "shd (szip s1 s2) = (shd s1, shd s2)"
-| "stl (szip s1 s2) = szip (stl s1) (stl s2)"
-
-lemma szip_unfold[code]: "szip (a ## s1) (b ## s2) = (a, b) ## (szip s1 s2)"
-  by (subst szip.ctr) simp
-
-lemma snth_szip[simp]: "szip s1 s2 !! n = (s1 !! n, s2 !! n)"
-  by (induct n arbitrary: s1 s2) auto
-
-lemma stake_szip[simp]:
-  "stake n (szip s1 s2) = zip (stake n s1) (stake n s2)"
-  by (induct n arbitrary: s1 s2) auto
-
-lemma sdrop_szip[simp]: "sdrop n (szip s1 s2) = szip (sdrop n s1) (sdrop n s2)"
-  by (induct n arbitrary: s1 s2) auto
-
-lemma smap_szip_fst:
-  "smap (\<lambda>x. f (fst x)) (szip s1 s2) = smap f s1"
-  by (coinduction arbitrary: s1 s2) auto
-
-lemma smap_szip_snd:
-  "smap (\<lambda>x. g (snd x)) (szip s1 s2) = smap g s2"
-  by (coinduction arbitrary: s1 s2) auto
-
-
-subsection {* zip via function *}
-
-primcorec smap2 where
-  "shd (smap2 f s1 s2) = f (shd s1) (shd s2)"
-| "stl (smap2 f s1 s2) = smap2 f (stl s1) (stl s2)"
-
-lemma smap2_unfold[code]:
-  "smap2 f (a ## s1) (b ## s2) = f a b ## (smap2 f s1 s2)"
-  by (subst smap2.ctr) simp
-
-lemma smap2_szip:
-  "smap2 f s1 s2 = smap (split f) (szip s1 s2)"
-  by (coinduction arbitrary: s1 s2) auto
-
-lemma smap_smap2[simp]:
-  "smap f (smap2 g s1 s2) = smap2 (\<lambda>x y. f (g x y)) s1 s2"
-  unfolding smap2_szip stream.map_comp o_def split_def ..
-
-lemma smap2_alt:
-  "(smap2 f s1 s2 = s) = (\<forall>n. f (s1 !! n) (s2 !! n) = s !! n)"
-  unfolding smap2_szip smap_alt by auto
-
-lemma snth_smap2[simp]:
-  "smap2 f s1 s2 !! n = f (s1 !! n) (s2 !! n)"
-  by (induct n arbitrary: s1 s2) auto
-
-lemma stake_smap2[simp]:
-  "stake n (smap2 f s1 s2) = map (split f) (zip (stake n s1) (stake n s2))"
-  by (induct n arbitrary: s1 s2) auto
-
-lemma sdrop_smap2[simp]:
-  "sdrop n (smap2 f s1 s2) = smap2 f (sdrop n s1) (sdrop n s2)"
-  by (induct n arbitrary: s1 s2) auto
-
-end
diff -r 7338eb25226c -r c38d8f139bbc src/HOL/Datatype_Examples/Stream_Processor.thy
--- a/src/HOL/Datatype_Examples/Stream_Processor.thy	Tue Oct 07 20:59:46 2014 +0200
+++ b/src/HOL/Datatype_Examples/Stream_Processor.thy	Tue Oct 07 21:01:31 2014 +0200
@@ -9,7 +9,7 @@
 header {* Stream Processors---A Syntactic Representation of Continuous Functions on Streams *}
 
 theory Stream_Processor
-imports Stream "~~/src/HOL/Library/BNF_Axiomatization"
+imports "~~/src/HOL/Library/Stream" "~~/src/HOL/Library/BNF_Axiomatization"
 begin
 
 section {* Continuous Functions on Streams *}
diff -r 7338eb25226c -r c38d8f139bbc src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Tue Oct 07 20:59:46 2014 +0200
+++ b/src/HOL/Library/FuncSet.thy	Tue Oct 07 21:01:31 2014 +0200
@@ -199,6 +199,9 @@
     "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> (\<lambda>x\<in>A. f x) = (\<lambda>x\<in>A. g x)"
   by (simp add: fun_eq_iff Pi_def restrict_def)
 
+lemma restrict_UNIV: "restrict f UNIV = f"
+  by (simp add: restrict_def)
+
 lemma inj_on_restrict_eq [simp]: "inj_on (restrict f A) A = inj_on f A"
   by (simp add: inj_on_def restrict_def)
 
diff -r 7338eb25226c -r c38d8f139bbc src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Tue Oct 07 20:59:46 2014 +0200
+++ b/src/HOL/Library/Library.thy	Tue Oct 07 21:01:31 2014 +0200
@@ -65,6 +65,7 @@
   Saturated
   Set_Algebras
   State_Monad
+  Stream
   Sublist
   Sum_of_Squares
   Transitive_Closure_Table
diff -r 7338eb25226c -r c38d8f139bbc src/HOL/Library/Stream.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Stream.thy	Tue Oct 07 21:01:31 2014 +0200
@@ -0,0 +1,582 @@
+(*  Title:      HOL/Library/Stream.thy
+    Author:     Dmitriy Traytel, TU Muenchen
+    Author:     Andrei Popescu, TU Muenchen
+    Copyright   2012, 2013
+
+Infinite streams.
+*)
+
+header {* Infinite Streams *}
+
+theory Stream
+imports "~~/src/HOL/Library/Nat_Bijection"
+begin
+
+codatatype (sset: 'a) stream =
+  SCons (shd: 'a) (stl: "'a stream") (infixr "##" 65)
+for
+  map: smap
+  rel: stream_all2
+
+(*for code generation only*)
+definition smember :: "'a \<Rightarrow> 'a stream \<Rightarrow> bool" where
+  [code_abbrev]: "smember x s \<longleftrightarrow> x \<in> sset s"
+
+lemma smember_code[code, simp]: "smember x (y ## s) = (if x = y then True else smember x s)"
+  unfolding smember_def by auto
+
+hide_const (open) smember
+
+lemmas smap_simps[simp] = stream.map_sel
+lemmas shd_sset = stream.set_sel(1)
+lemmas stl_sset = stream.set_sel(2)
+
+theorem sset_induct[consumes 1, case_names shd stl, induct set: sset]:
+  assumes "y \<in> sset s" and "\<And>s. P (shd s) s" and "\<And>s y. \<lbrakk>y \<in> sset (stl s); P y (stl s)\<rbrakk> \<Longrightarrow> P y s"
+  shows "P y s"
+using assms by induct (metis stream.sel(1), auto)
+
+
+subsection {* prepend list to stream *}
+
+primrec shift :: "'a list \<Rightarrow> 'a stream \<Rightarrow> 'a stream" (infixr "@-" 65) where
+  "shift [] s = s"
+| "shift (x # xs) s = x ## shift xs s"
+
+lemma smap_shift[simp]: "smap f (xs @- s) = map f xs @- smap f s"
+  by (induct xs) auto
+
+lemma shift_append[simp]: "(xs @ ys) @- s = xs @- ys @- s"
+  by (induct xs) auto
+
+lemma shift_simps[simp]:
+   "shd (xs @- s) = (if xs = [] then shd s else hd xs)"
+   "stl (xs @- s) = (if xs = [] then stl s else tl xs @- s)"
+  by (induct xs) auto
+
+lemma sset_shift[simp]: "sset (xs @- s) = set xs \<union> sset s"
+  by (induct xs) auto
+
+lemma shift_left_inj[simp]: "xs @- s1 = xs @- s2 \<longleftrightarrow> s1 = s2"
+  by (induct xs) auto
+
+
+subsection {* set of streams with elements in some fixed set *}
+
+coinductive_set
+  streams :: "'a set \<Rightarrow> 'a stream set"
+  for A :: "'a set"
+where
+  Stream[intro!, simp, no_atp]: "\<lbrakk>a \<in> A; s \<in> streams A\<rbrakk> \<Longrightarrow> a ## s \<in> streams A"
+
+lemma shift_streams: "\<lbrakk>w \<in> lists A; s \<in> streams A\<rbrakk> \<Longrightarrow> w @- s \<in> streams A"
+  by (induct w) auto
+
+lemma streams_Stream: "x ## s \<in> streams A \<longleftrightarrow> x \<in> A \<and> s \<in> streams A"
+  by (auto elim: streams.cases)
+
+lemma streams_stl: "s \<in> streams A \<Longrightarrow> stl s \<in> streams A"
+  by (cases s) (auto simp: streams_Stream)
+
+lemma streams_shd: "s \<in> streams A \<Longrightarrow> shd s \<in> A"
+  by (cases s) (auto simp: streams_Stream)
+
+lemma sset_streams:
+  assumes "sset s \<subseteq> A"
+  shows "s \<in> streams A"
+using assms proof (coinduction arbitrary: s)
+  case streams then show ?case by (cases s) simp
+qed
+
+lemma streams_sset:
+  assumes "s \<in> streams A"
+  shows "sset s \<subseteq> A"
+proof
+  fix x assume "x \<in> sset s" from this `s \<in> streams A` show "x \<in> A"
+    by (induct s) (auto intro: streams_shd streams_stl)
+qed
+
+lemma streams_iff_sset: "s \<in> streams A \<longleftrightarrow> sset s \<subseteq> A"
+  by (metis sset_streams streams_sset)
+
+lemma streams_mono:  "s \<in> streams A \<Longrightarrow> A \<subseteq> B \<Longrightarrow> s \<in> streams B"
+  unfolding streams_iff_sset by auto
+
+lemma smap_streams: "s \<in> streams A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<in> B) \<Longrightarrow> smap f s \<in> streams B"
+  unfolding streams_iff_sset stream.set_map by auto
+
+lemma streams_empty: "streams {} = {}"
+  by (auto elim: streams.cases)
+
+lemma streams_UNIV[simp]: "streams UNIV = UNIV"
+  by (auto simp: streams_iff_sset)
+
+subsection {* nth, take, drop for streams *}
+
+primrec snth :: "'a stream \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
+  "s !! 0 = shd s"
+| "s !! Suc n = stl s !! n"
+
+lemma snth_smap[simp]: "smap f s !! n = f (s !! n)"
+  by (induct n arbitrary: s) auto
+
+lemma shift_snth_less[simp]: "p < length xs \<Longrightarrow> (xs @- s) !! p = xs ! p"
+  by (induct p arbitrary: xs) (auto simp: hd_conv_nth nth_tl)
+
+lemma shift_snth_ge[simp]: "p \<ge> length xs \<Longrightarrow> (xs @- s) !! p = s !! (p - length xs)"
+  by (induct p arbitrary: xs) (auto simp: Suc_diff_eq_diff_pred)
+
+lemma shift_snth: "(xs @- s) !! n = (if n < length xs then xs ! n else s !! (n - length xs))"
+  by auto
+
+lemma snth_sset[simp]: "s !! n \<in> sset s"
+  by (induct n arbitrary: s) (auto intro: shd_sset stl_sset)
+
+lemma sset_range: "sset s = range (snth s)"
+proof (intro equalityI subsetI)
+  fix x assume "x \<in> sset s"
+  thus "x \<in> range (snth s)"
+  proof (induct s)
+    case (stl s x)
+    then obtain n where "x = stl s !! n" by auto
+    thus ?case by (auto intro: range_eqI[of _ _ "Suc n"])
+  qed (auto intro: range_eqI[of _ _ 0])
+qed auto
+
+primrec stake :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a list" where
+  "stake 0 s = []"
+| "stake (Suc n) s = shd s # stake n (stl s)"
+
+lemma length_stake[simp]: "length (stake n s) = n"
+  by (induct n arbitrary: s) auto
+
+lemma stake_smap[simp]: "stake n (smap f s) = map f (stake n s)"
+  by (induct n arbitrary: s) auto
+
+lemma take_stake: "take n (stake m s) = stake (min n m) s"
+proof (induct m arbitrary: s n)
+  case (Suc m) thus ?case by (cases n) auto
+qed simp
+
+primrec sdrop :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where
+  "sdrop 0 s = s"
+| "sdrop (Suc n) s = sdrop n (stl s)"
+
+lemma sdrop_simps[simp]:
+  "shd (sdrop n s) = s !! n" "stl (sdrop n s) = sdrop (Suc n) s"
+  by (induct n arbitrary: s)  auto
+
+lemma sdrop_smap[simp]: "sdrop n (smap f s) = smap f (sdrop n s)"
+  by (induct n arbitrary: s) auto
+
+lemma sdrop_stl: "sdrop n (stl s) = stl (sdrop n s)"
+  by (induct n) auto
+
+lemma drop_stake: "drop n (stake m s) = stake (m - n) (sdrop n s)"
+proof (induct m arbitrary: s n)
+  case (Suc m) thus ?case by (cases n) auto
+qed simp
+
+lemma stake_sdrop: "stake n s @- sdrop n s = s"
+  by (induct n arbitrary: s) auto
+
+lemma id_stake_snth_sdrop:
+  "s = stake i s @- s !! i ## sdrop (Suc i) s"
+  by (subst stake_sdrop[symmetric, of _ i]) (metis sdrop_simps stream.collapse)
+
+lemma smap_alt: "smap f s = s' \<longleftrightarrow> (\<forall>n. f (s !! n) = s' !! n)" (is "?L = ?R")
+proof
+  assume ?R
+  then have "\<And>n. smap f (sdrop n s) = sdrop n s'"
+    by coinduction (auto intro: exI[of _ 0] simp del: sdrop.simps(2))
+  then show ?L using sdrop.simps(1) by metis
+qed auto
+
+lemma stake_invert_Nil[iff]: "stake n s = [] \<longleftrightarrow> n = 0"
+  by (induct n) auto
+
+lemma sdrop_shift: "sdrop i (w @- s) = drop i w @- sdrop (i - length w) s"
+  by (induct i arbitrary: w s) (auto simp: drop_tl drop_Suc neq_Nil_conv)
+
+lemma stake_shift: "stake i (w @- s) = take i w @ stake (i - length w) s"
+  by (induct i arbitrary: w s) (auto simp: neq_Nil_conv)
+
+lemma stake_add[simp]: "stake m s @ stake n (sdrop m s) = stake (m + n) s"
+  by (induct m arbitrary: s) auto
+
+lemma sdrop_add[simp]: "sdrop n (sdrop m s) = sdrop (m + n) s"
+  by (induct m arbitrary: s) auto
+
+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 
+  "sdrop_while P s = (if P (shd s) then sdrop_while P (stl s) else s)"
+
+lemma sdrop_while_SCons[code]:
+  "sdrop_while P (a ## s) = (if P a then sdrop_while P s else a ## s)"
+  by (subst sdrop_while.simps) simp
+
+lemma sdrop_while_sdrop_LEAST:
+  assumes "\<exists>n. P (s !! n)"
+  shows "sdrop_while (Not o P) s = sdrop (LEAST n. P (s !! n)) s"
+proof -
+  from assms obtain m where "P (s !! m)" "\<And>n. P (s !! n) \<Longrightarrow> m \<le> n"
+    and *: "(LEAST n. P (s !! n)) = m" by atomize_elim (auto intro: LeastI Least_le)
+  thus ?thesis unfolding *
+  proof (induct m arbitrary: s)
+    case (Suc m)
+    hence "sdrop_while (Not \<circ> P) (stl s) = sdrop m (stl s)"
+      by (metis (full_types) not_less_eq_eq snth.simps(2))
+    moreover from Suc(3) have "\<not> (P (s !! 0))" by blast
+    ultimately show ?case by (subst sdrop_while.simps) simp
+  qed (metis comp_apply sdrop.simps(1) sdrop_while.simps snth.simps(1))
+qed
+
+primcorec sfilter where
+  "shd (sfilter P s) = shd (sdrop_while (Not o P) s)"
+| "stl (sfilter P s) = sfilter P (stl (sdrop_while (Not o P) s))"
+
+lemma sfilter_Stream: "sfilter P (x ## s) = (if P x then x ## sfilter P s else sfilter P s)"
+proof (cases "P x")
+  case True thus ?thesis by (subst sfilter.ctr) (simp add: sdrop_while_SCons)
+next
+  case False thus ?thesis by (subst (1 2) sfilter.ctr) (simp add: sdrop_while_SCons)
+qed
+
+
+subsection {* unary predicates lifted to streams *}
+
+definition "stream_all P s = (\<forall>p. P (s !! p))"
+
+lemma stream_all_iff[iff]: "stream_all P s \<longleftrightarrow> Ball (sset s) P"
+  unfolding stream_all_def sset_range by auto
+
+lemma stream_all_shift[simp]: "stream_all P (xs @- s) = (list_all P xs \<and> stream_all P s)"
+  unfolding stream_all_iff list_all_iff by auto
+
+lemma stream_all_Stream: "stream_all P (x ## X) \<longleftrightarrow> P x \<and> stream_all P X"
+  by simp
+
+
+subsection {* recurring stream out of a list *}
+
+primcorec cycle :: "'a list \<Rightarrow> 'a stream" where
+  "shd (cycle xs) = hd xs"
+| "stl (cycle xs) = cycle (tl xs @ [hd xs])"
+
+lemma cycle_decomp: "u \<noteq> [] \<Longrightarrow> cycle u = u @- cycle u"
+proof (coinduction arbitrary: u)
+  case Eq_stream then show ?case using stream.collapse[of "cycle u"]
+    by (auto intro!: exI[of _ "tl u @ [hd u]"])
+qed
+
+lemma cycle_Cons[code]: "cycle (x # xs) = x ## cycle (xs @ [x])"
+  by (subst cycle.ctr) simp
+
+lemma cycle_rotated: "\<lbrakk>v \<noteq> []; cycle u = v @- s\<rbrakk> \<Longrightarrow> cycle (tl u @ [hd u]) = tl v @- s"
+  by (auto dest: arg_cong[of _ _ stl])
+
+lemma stake_append: "stake n (u @- s) = take (min (length u) n) u @ stake (n - length u) s"
+proof (induct n arbitrary: u)
+  case (Suc n) thus ?case by (cases u) auto
+qed auto
+
+lemma stake_cycle_le[simp]:
+  assumes "u \<noteq> []" "n < length u"
+  shows "stake n (cycle u) = take n u"
+using min_absorb2[OF less_imp_le_nat[OF assms(2)]]
+  by (subst cycle_decomp[OF assms(1)], subst stake_append) auto
+
+lemma stake_cycle_eq[simp]: "u \<noteq> [] \<Longrightarrow> stake (length u) (cycle u) = u"
+  by (subst cycle_decomp) (auto simp: stake_shift)
+
+lemma sdrop_cycle_eq[simp]: "u \<noteq> [] \<Longrightarrow> sdrop (length u) (cycle u) = cycle u"
+  by (subst cycle_decomp) (auto simp: sdrop_shift)
+
+lemma stake_cycle_eq_mod_0[simp]: "\<lbrakk>u \<noteq> []; n mod length u = 0\<rbrakk> \<Longrightarrow>
+   stake n (cycle u) = concat (replicate (n div length u) u)"
+  by (induct "n div length u" arbitrary: n u) (auto simp: stake_add[symmetric])
+
+lemma sdrop_cycle_eq_mod_0[simp]: "\<lbrakk>u \<noteq> []; n mod length u = 0\<rbrakk> \<Longrightarrow>
+   sdrop n (cycle u) = cycle u"
+  by (induct "n div length u" arbitrary: n u) (auto simp: sdrop_add[symmetric])
+
+lemma stake_cycle: "u \<noteq> [] \<Longrightarrow>
+   stake n (cycle u) = concat (replicate (n div length u) u) @ take (n mod length u) u"
+  by (subst mod_div_equality[of n "length u", symmetric], unfold stake_add[symmetric]) auto
+
+lemma sdrop_cycle: "u \<noteq> [] \<Longrightarrow> sdrop n (cycle u) = cycle (rotate (n mod length u) u)"
+  by (induct n arbitrary: u) (auto simp: rotate1_rotate_swap rotate1_hd_tl rotate_conv_mod[symmetric])
+
+
+subsection {* iterated application of a function *}
+
+primcorec siterate where
+  "shd (siterate f x) = x"
+| "stl (siterate f x) = siterate f (f x)"
+
+lemma stake_Suc: "stake (Suc n) s = stake n s @ [s !! n]"
+  by (induct n arbitrary: s) auto
+
+lemma snth_siterate[simp]: "siterate f x !! n = (f^^n) x"
+  by (induct n arbitrary: x) (auto simp: funpow_swap1)
+
+lemma sdrop_siterate[simp]: "sdrop n (siterate f x) = siterate f ((f^^n) x)"
+  by (induct n arbitrary: x) (auto simp: funpow_swap1)
+
+lemma stake_siterate[simp]: "stake n (siterate f x) = map (\<lambda>n. (f^^n) x) [0 ..< n]"
+  by (induct n arbitrary: x) (auto simp del: stake.simps(2) simp: stake_Suc)
+
+lemma sset_siterate: "sset (siterate f x) = {(f^^n) x | n. True}"
+  by (auto simp: sset_range)
+
+lemma smap_siterate: "smap f (siterate f x) = siterate f (f x)"
+  by (coinduction arbitrary: x) auto
+
+
+subsection {* stream repeating a single element *}
+
+abbreviation "sconst \<equiv> siterate id"
+
+lemma shift_replicate_sconst[simp]: "replicate n x @- sconst x = sconst x"
+  by (subst (3) stake_sdrop[symmetric]) (simp add: map_replicate_trivial)
+
+lemma sset_sconst[simp]: "sset (sconst x) = {x}"
+  by (simp add: sset_siterate)
+
+lemma sconst_alt: "s = sconst x \<longleftrightarrow> sset s = {x}"
+proof
+  assume "sset s = {x}"
+  then show "s = sconst x"
+  proof (coinduction arbitrary: s)
+    case Eq_stream
+    then have "shd s = x" "sset (stl s) \<subseteq> {x}" by (case_tac [!] s) auto
+    then have "sset (stl s) = {x}" by (cases "stl s") auto
+    with `shd s = x` show ?case by auto
+  qed
+qed simp
+
+lemma same_cycle: "sconst x = cycle [x]"
+  by coinduction auto
+
+lemma smap_sconst: "smap f (sconst x) = sconst (f x)"
+  by coinduction auto
+
+lemma sconst_streams: "x \<in> A \<Longrightarrow> sconst x \<in> streams A"
+  by (simp add: streams_iff_sset)
+
+
+subsection {* stream of natural numbers *}
+
+abbreviation "fromN \<equiv> siterate Suc"
+
+abbreviation "nats \<equiv> fromN 0"
+
+lemma sset_fromN[simp]: "sset (fromN n) = {n ..}"
+  by (auto simp add: sset_siterate le_iff_add)
+
+lemma stream_smap_fromN: "s = smap (\<lambda>j. let i = j - n in s !! i) (fromN n)"
+  by (coinduction arbitrary: s n)
+    (force simp: neq_Nil_conv Let_def snth.simps(2)[symmetric] Suc_diff_Suc
+      intro: stream.map_cong split: if_splits simp del: snth.simps(2))
+
+lemma stream_smap_nats: "s = smap (snth s) nats"
+  using stream_smap_fromN[where n = 0] by simp
+
+
+subsection {* flatten a stream of lists *}
+
+primcorec flat where
+  "shd (flat ws) = hd (shd ws)"
+| "stl (flat ws) = flat (if tl (shd ws) = [] then stl ws else tl (shd ws) ## stl ws)"
+
+lemma flat_Cons[simp, code]: "flat ((x # xs) ## ws) = x ## flat (if xs = [] then ws else xs ## ws)"
+  by (subst flat.ctr) simp
+
+lemma flat_Stream[simp]: "xs \<noteq> [] \<Longrightarrow> flat (xs ## ws) = xs @- flat ws"
+  by (induct xs) auto
+
+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 
+  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> 
+  sset (flat s) = (\<Union>xs \<in> sset s. set xs)" (is "?P \<Longrightarrow> ?L = ?R")
+proof safe
+  fix x assume ?P "x : ?L"
+  then obtain m where "x = flat s !! m" by (metis image_iff sset_range)
+  with `?P` obtain n m' where "x = s !! n ! m'" "m' < length (s !! n)"
+  proof (atomize_elim, induct m arbitrary: s rule: less_induct)
+    case (less y)
+    thus ?case
+    proof (cases "y < length (shd s)")
+      case True thus ?thesis by (metis flat_snth less(2,3) snth.simps(1))
+    next
+      case False
+      hence "x = flat (stl s) !! (y - length (shd s))" by (metis less(2,3) flat_snth)
+      moreover
+      { from less(2) have *: "length (shd s) > 0" by (cases s) simp_all
+        with False have "y > 0" by (cases y) simp_all
+        with * have "y - length (shd s) < y" by simp
+      }
+      moreover have "\<forall>xs \<in> sset (stl s). xs \<noteq> []" using less(2) by (cases s) auto
+      ultimately have "\<exists>n m'. x = stl s !! n ! m' \<and> m' < length (stl s !! n)" by (intro less(1)) auto
+      thus ?thesis by (metis snth.simps(2))
+    qed
+  qed
+  thus "x \<in> ?R" by (auto simp: sset_range dest!: nth_mem)
+next
+  fix x xs assume "xs \<in> sset s" ?P "x \<in> set xs" thus "x \<in> ?L"
+    by (induct rule: sset_induct)
+      (metis UnI1 flat_unfold shift.simps(1) sset_shift,
+       metis UnI2 flat_unfold shd_sset stl_sset sset_shift)
+qed
+
+
+subsection {* merge a stream of streams *}
+
+definition smerge :: "'a stream stream \<Rightarrow> 'a stream" where
+  "smerge ss = flat (smap (\<lambda>n. map (\<lambda>s. s !! n) (stake (Suc n) ss) @ stake n (ss !! n)) nats)"
+
+lemma stake_nth[simp]: "m < n \<Longrightarrow> stake n s ! m = s !! m"
+  by (induct n arbitrary: s m) (auto simp: nth_Cons', metis Suc_pred snth.simps(2))
+
+lemma snth_sset_smerge: "ss !! n !! m \<in> sset (smerge ss)"
+proof (cases "n \<le> m")
+  case False thus ?thesis unfolding smerge_def
+    by (subst sset_flat)
+      (auto simp: stream.set_map in_set_conv_nth simp del: stake.simps
+        intro!: exI[of _ n, OF disjI2] exI[of _ m, OF mp])
+next
+  case True thus ?thesis unfolding smerge_def
+    by (subst sset_flat)
+      (auto simp: stream.set_map in_set_conv_nth image_iff simp del: stake.simps snth.simps
+        intro!: exI[of _ m, OF disjI1] bexI[of _ "ss !! n"] exI[of _ n, OF mp])
+qed
+
+lemma sset_smerge: "sset (smerge ss) = UNION (sset ss) sset"
+proof safe
+  fix x assume "x \<in> sset (smerge ss)"
+  thus "x \<in> UNION (sset ss) sset"
+    unfolding smerge_def by (subst (asm) sset_flat)
+      (auto simp: stream.set_map in_set_conv_nth sset_range simp del: stake.simps, fast+)
+next
+  fix s x assume "s \<in> sset ss" "x \<in> sset s"
+  thus "x \<in> sset (smerge ss)" using snth_sset_smerge by (auto simp: sset_range)
+qed
+
+
+subsection {* product of two streams *}
+
+definition sproduct :: "'a stream \<Rightarrow> 'b stream \<Rightarrow> ('a \<times> 'b) stream" where
+  "sproduct s1 s2 = smerge (smap (\<lambda>x. smap (Pair x) s2) s1)"
+
+lemma sset_sproduct: "sset (sproduct s1 s2) = sset s1 \<times> sset s2"
+  unfolding sproduct_def sset_smerge by (auto simp: stream.set_map)
+
+
+subsection {* interleave two streams *}
+
+primcorec sinterleave where
+  "shd (sinterleave s1 s2) = shd s1"
+| "stl (sinterleave s1 s2) = sinterleave s2 (stl s1)"
+
+lemma sinterleave_code[code]:
+  "sinterleave (x ## s1) s2 = x ## sinterleave s2 s1"
+  by (subst sinterleave.ctr) simp
+
+lemma sinterleave_snth[simp]:
+  "even n \<Longrightarrow> sinterleave s1 s2 !! n = s1 !! (n div 2)"
+   "odd n \<Longrightarrow> sinterleave s1 s2 !! n = s2 !! (n div 2)"
+  by (induct n arbitrary: s1 s2)
+    (auto dest: even_nat_Suc_div_2 odd_nat_plus_one_div_two[folded nat_2])
+
+lemma sset_sinterleave: "sset (sinterleave s1 s2) = sset s1 \<union> sset s2"
+proof (intro equalityI subsetI)
+  fix x assume "x \<in> sset (sinterleave s1 s2)"
+  then obtain n where "x = sinterleave s1 s2 !! n" unfolding sset_range by blast
+  thus "x \<in> sset s1 \<union> sset s2" by (cases "even n") auto
+next
+  fix x assume "x \<in> sset s1 \<union> sset s2"
+  thus "x \<in> sset (sinterleave s1 s2)"
+  proof
+    assume "x \<in> sset s1"
+    then obtain n where "x = s1 !! n" unfolding sset_range by blast
+    hence "sinterleave s1 s2 !! (2 * n) = x" by simp
+    thus ?thesis unfolding sset_range by blast
+  next
+    assume "x \<in> sset s2"
+    then obtain n where "x = s2 !! n" unfolding sset_range by blast
+    hence "sinterleave s1 s2 !! (2 * n + 1) = x" by simp
+    thus ?thesis unfolding sset_range by blast
+  qed
+qed
+
+
+subsection {* zip *}
+
+primcorec szip where
+  "shd (szip s1 s2) = (shd s1, shd s2)"
+| "stl (szip s1 s2) = szip (stl s1) (stl s2)"
+
+lemma szip_unfold[code]: "szip (a ## s1) (b ## s2) = (a, b) ## (szip s1 s2)"
+  by (subst szip.ctr) simp
+
+lemma snth_szip[simp]: "szip s1 s2 !! n = (s1 !! n, s2 !! n)"
+  by (induct n arbitrary: s1 s2) auto
+
+lemma stake_szip[simp]:
+  "stake n (szip s1 s2) = zip (stake n s1) (stake n s2)"
+  by (induct n arbitrary: s1 s2) auto
+
+lemma sdrop_szip[simp]: "sdrop n (szip s1 s2) = szip (sdrop n s1) (sdrop n s2)"
+  by (induct n arbitrary: s1 s2) auto
+
+lemma smap_szip_fst:
+  "smap (\<lambda>x. f (fst x)) (szip s1 s2) = smap f s1"
+  by (coinduction arbitrary: s1 s2) auto
+
+lemma smap_szip_snd:
+  "smap (\<lambda>x. g (snd x)) (szip s1 s2) = smap g s2"
+  by (coinduction arbitrary: s1 s2) auto
+
+
+subsection {* zip via function *}
+
+primcorec smap2 where
+  "shd (smap2 f s1 s2) = f (shd s1) (shd s2)"
+| "stl (smap2 f s1 s2) = smap2 f (stl s1) (stl s2)"
+
+lemma smap2_unfold[code]:
+  "smap2 f (a ## s1) (b ## s2) = f a b ## (smap2 f s1 s2)"
+  by (subst smap2.ctr) simp
+
+lemma smap2_szip:
+  "smap2 f s1 s2 = smap (split f) (szip s1 s2)"
+  by (coinduction arbitrary: s1 s2) auto
+
+lemma smap_smap2[simp]:
+  "smap f (smap2 g s1 s2) = smap2 (\<lambda>x y. f (g x y)) s1 s2"
+  unfolding smap2_szip stream.map_comp o_def split_def ..
+
+lemma smap2_alt:
+  "(smap2 f s1 s2 = s) = (\<forall>n. f (s1 !! n) (s2 !! n) = s !! n)"
+  unfolding smap2_szip smap_alt by auto
+
+lemma snth_smap2[simp]:
+  "smap2 f s1 s2 !! n = f (s1 !! n) (s2 !! n)"
+  by (induct n arbitrary: s1 s2) auto
+
+lemma stake_smap2[simp]:
+  "stake n (smap2 f s1 s2) = map (split f) (zip (stake n s1) (stake n s2))"
+  by (induct n arbitrary: s1 s2) auto
+
+lemma sdrop_smap2[simp]:
+  "sdrop n (smap2 f s1 s2) = smap2 f (sdrop n s1) (sdrop n s2)"
+  by (induct n arbitrary: s1 s2) auto
+
+end
diff -r 7338eb25226c -r c38d8f139bbc src/HOL/Probability/Binary_Product_Measure.thy
--- a/src/HOL/Probability/Binary_Product_Measure.thy	Tue Oct 07 20:59:46 2014 +0200
+++ b/src/HOL/Probability/Binary_Product_Measure.thy	Tue Oct 07 21:01:31 2014 +0200
@@ -34,6 +34,12 @@
   unfolding pair_measure_def using pair_measure_closed[of A B]
   by (rule sets_measure_of)
 
+lemma sets_pair_in_sets:
+  assumes N: "space A \<times> space B = space N"
+  assumes "\<And>a b. a \<in> sets A \<Longrightarrow> b \<in> sets B \<Longrightarrow> a \<times> b \<in> sets N"
+  shows "sets (A \<Otimes>\<^sub>M B) \<subseteq> sets N"
+  using assms by (auto intro!: sets.sigma_sets_subset simp: sets_pair_measure N)
+
 lemma sets_pair_measure_cong[cong]:
   "sets M1 = sets M1' \<Longrightarrow> sets M2 = sets M2' \<Longrightarrow> sets (M1 \<Otimes>\<^sub>M M2) = sets (M1' \<Otimes>\<^sub>M M2')"
   unfolding sets_pair_measure by (simp cong: sets_eq_imp_space_eq)
@@ -42,6 +48,9 @@
   "x \<in> sets A \<Longrightarrow> y \<in> sets B \<Longrightarrow> x \<times> y \<in> sets (A \<Otimes>\<^sub>M B)"
   by (auto simp: sets_pair_measure)
 
+lemma sets_Pair: "{x} \<in> sets M1 \<Longrightarrow> {y} \<in> sets M2 \<Longrightarrow> {(x, y)} \<in> sets (M1 \<Otimes>\<^sub>M M2)"
+  using pair_measureI[of "{x}" M1 "{y}" M2] by simp
+
 lemma measurable_pair_measureI:
   assumes 1: "f \<in> space M \<rightarrow> space M1 \<times> space M2"
   assumes 2: "\<And>A B. A \<in> sets M1 \<Longrightarrow> B \<in> sets M2 \<Longrightarrow> f -` (A \<times> B) \<inter> space M \<in> sets M"
@@ -98,6 +107,25 @@
     and measurable_snd'': "(\<lambda>x. f (snd x)) \<in> measurable (P \<Otimes>\<^sub>M M) N"
   by simp_all
 
+lemma sets_pair_eq_sets_fst_snd:
+  "sets (A \<Otimes>\<^sub>M B) = sets (Sup_sigma {vimage_algebra (space A \<times> space B) fst A, vimage_algebra (space A \<times> space B) snd B})"
+    (is "?P = sets (Sup_sigma {?fst, ?snd})")
+proof -
+  { fix a b assume ab: "a \<in> sets A" "b \<in> sets B"
+    then have "a \<times> b = (fst -` a \<inter> (space A \<times> space B)) \<inter> (snd -` b \<inter> (space A \<times> space B))"
+      by (auto dest: sets.sets_into_space)
+    also have "\<dots> \<in> sets (Sup_sigma {?fst, ?snd})"
+      using ab by (auto intro: in_Sup_sigma in_vimage_algebra)
+    finally have "a \<times> b \<in> sets (Sup_sigma {?fst, ?snd})" . }
+  moreover have "sets ?fst \<subseteq> sets (A \<Otimes>\<^sub>M B)"
+    by (rule sets_image_in_sets) (auto simp: space_pair_measure[symmetric])
+  moreover have "sets ?snd \<subseteq> sets (A \<Otimes>\<^sub>M B)"  
+    by (rule sets_image_in_sets) (auto simp: space_pair_measure)
+  ultimately show ?thesis
+    by (intro antisym[of "sets A" for A] sets_Sup_in_sets sets_pair_in_sets )
+       (auto simp add: space_Sup_sigma space_pair_measure)
+qed
+
 lemma measurable_pair_iff:
   "f \<in> measurable M (M1 \<Otimes>\<^sub>M M2) \<longleftrightarrow> (fst \<circ> f) \<in> measurable M M1 \<and> (snd \<circ> f) \<in> measurable M M2"
   by (auto intro: measurable_pair[of f M M1 M2]) 
diff -r 7338eb25226c -r c38d8f139bbc src/HOL/Probability/Finite_Product_Measure.thy
--- a/src/HOL/Probability/Finite_Product_Measure.thy	Tue Oct 07 20:59:46 2014 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Tue Oct 07 21:01:31 2014 +0200
@@ -353,6 +353,25 @@
   finally show "A \<in> sigma_sets ?\<Omega> (prod_algebra I M)" .
 qed
 
+lemma sets_PiM_eq_proj:
+  "I \<noteq> {} \<Longrightarrow> sets (PiM I M) = sets (\<Squnion>\<^sub>\<sigma> i\<in>I. vimage_algebra (\<Pi>\<^sub>E i\<in>I. space (M i)) (\<lambda>x. x i) (M i))"
+  apply (simp add: sets_PiM_single sets_Sup_sigma)
+  apply (subst SUP_cong[OF refl])
+  apply (rule sets_vimage_algebra2)
+  apply auto []
+  apply (auto intro!: arg_cong2[where f=sigma_sets])
+  done
+
+lemma sets_PiM_in_sets:
+  assumes space: "space N = (\<Pi>\<^sub>E i\<in>I. space (M i))"
+  assumes sets: "\<And>i A. i \<in> I \<Longrightarrow> A \<in> sets (M i) \<Longrightarrow> {x\<in>space N. x i \<in> A} \<in> sets N"
+  shows "sets (\<Pi>\<^sub>M i \<in> I. M i) \<subseteq> sets N"
+  unfolding sets_PiM_single space[symmetric]
+  by (intro sets.sigma_sets_subset subsetI) (auto intro: sets)
+
+lemma sets_PiM_cong: assumes "I = J" "\<And>i. i \<in> J \<Longrightarrow> sets (M i) = sets (N i)" shows "sets (PiM I M) = sets (PiM J N)"
+  using assms sets_eq_imp_space_eq[OF assms(2)] by (simp add: sets_PiM_single cong: PiE_cong conj_cong)
+
 lemma sets_PiM_I:
   assumes "finite J" "J \<subseteq> I" "\<forall>i\<in>J. E i \<in> sets (M i)"
   shows "prod_emb I M J (PIE j:J. E j) \<in> sets (PIM i:I. M i)"
diff -r 7338eb25226c -r c38d8f139bbc src/HOL/Probability/Giry_Monad.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Giry_Monad.thy	Tue Oct 07 21:01:31 2014 +0200
@@ -0,0 +1,868 @@
+(*  Title:      HOL/Probability/Giry_Monad.thy
+    Author:     Johannes Hölzl, TU München
+    Author:     Manuel Eberl, TU München
+
+Defines the subprobability spaces, the subprobability functor and the Giry monad on subprobability
+spaces.
+*)
+
+theory Giry_Monad
+  imports Probability_Measure "~~/src/HOL/Library/Monad_Syntax"
+begin
+
+section {* Sub-probability spaces *}
+
+locale subprob_space = finite_measure +
+  assumes emeasure_space_le_1: "emeasure M (space M) \<le> 1"
+  assumes subprob_not_empty: "space M \<noteq> {}"
+
+lemma subprob_spaceI[Pure.intro!]:
+  assumes *: "emeasure M (space M) \<le> 1"
+  assumes "space M \<noteq> {}"
+  shows "subprob_space M"
+proof -
+  interpret finite_measure M
+  proof
+    show "emeasure M (space M) \<noteq> \<infinity>" using * by auto
+  qed
+  show "subprob_space M" by default fact+
+qed
+
+lemma prob_space_imp_subprob_space:
+  "prob_space M \<Longrightarrow> subprob_space M"
+  by (rule subprob_spaceI) (simp_all add: prob_space.emeasure_space_1 prob_space.not_empty)
+
+sublocale prob_space \<subseteq> subprob_space
+  by (rule subprob_spaceI) (simp_all add: emeasure_space_1 not_empty)
+
+lemma (in subprob_space) subprob_space_distr:
+  assumes f: "f \<in> measurable M M'" and "space M' \<noteq> {}" shows "subprob_space (distr M M' f)"
+proof (rule subprob_spaceI)
+  have "f -` space M' \<inter> space M = space M" using f by (auto dest: measurable_space)
+  with f show "emeasure (distr M M' f) (space (distr M M' f)) \<le> 1"
+    by (auto simp: emeasure_distr emeasure_space_le_1)
+  show "space (distr M M' f) \<noteq> {}" by (simp add: assms)
+qed
+
+lemma (in subprob_space) subprob_measure_le_1: "emeasure M X \<le> 1"
+  by (rule order.trans[OF emeasure_space emeasure_space_le_1])
+
+locale pair_subprob_space = 
+  pair_sigma_finite M1 M2 + M1: subprob_space M1 + M2: subprob_space M2 for M1 M2
+
+sublocale pair_subprob_space \<subseteq> P: subprob_space "M1 \<Otimes>\<^sub>M M2"
+proof
+  have "\<And>a b. \<lbrakk>a \<ge> 0; b \<ge> 0; a \<le> 1; b \<le> 1\<rbrakk> \<Longrightarrow> a * b \<le> (1::ereal)"
+    by (metis comm_monoid_mult_class.mult.left_neutral dual_order.trans ereal_mult_right_mono)
+  from this[OF _ _ M1.emeasure_space_le_1 M2.emeasure_space_le_1]
+    show "emeasure (M1 \<Otimes>\<^sub>M M2) (space (M1 \<Otimes>\<^sub>M M2)) \<le> 1"
+    by (simp add: M2.emeasure_pair_measure_Times space_pair_measure emeasure_nonneg)
+  from M1.subprob_not_empty and M2.subprob_not_empty show "space (M1 \<Otimes>\<^sub>M M2) \<noteq> {}"
+    by (simp add: space_pair_measure)
+qed
+
+definition subprob_algebra :: "'a measure \<Rightarrow> 'a measure measure" where
+  "subprob_algebra K =
+    (\<Squnion>\<^sub>\<sigma> A\<in>sets K. vimage_algebra {M. subprob_space M \<and> sets M = sets K} (\<lambda>M. emeasure M A) borel)"
+
+lemma space_subprob_algebra: "space (subprob_algebra A) = {M. subprob_space M \<and> sets M = sets A}"
+  by (auto simp add: subprob_algebra_def space_Sup_sigma)
+
+lemma subprob_algebra_cong: "sets M = sets N \<Longrightarrow> subprob_algebra M = subprob_algebra N"
+  by (simp add: subprob_algebra_def)
+
+lemma measurable_emeasure_subprob_algebra[measurable]: 
+  "a \<in> sets A \<Longrightarrow> (\<lambda>M. emeasure M a) \<in> borel_measurable (subprob_algebra A)"
+  by (auto intro!: measurable_Sup_sigma1 measurable_vimage_algebra1 simp: subprob_algebra_def)
+
+context
+  fixes K M N assumes K: "K \<in> measurable M (subprob_algebra N)"
+begin
+
+lemma subprob_space_kernel: "a \<in> space M \<Longrightarrow> subprob_space (K a)"
+  using measurable_space[OF K] by (simp add: space_subprob_algebra)
+
+lemma sets_kernel: "a \<in> space M \<Longrightarrow> sets (K a) = sets N"
+  using measurable_space[OF K] by (simp add: space_subprob_algebra)
+
+lemma measurable_emeasure_kernel[measurable]: 
+    "A \<in> sets N \<Longrightarrow> (\<lambda>a. emeasure (K a) A) \<in> borel_measurable M"
+  using measurable_compose[OF K measurable_emeasure_subprob_algebra] .
+
+end
+
+lemma measurable_subprob_algebra:
+  "(\<And>a. a \<in> space M \<Longrightarrow> subprob_space (K a)) \<Longrightarrow>
+  (\<And>a. a \<in> space M \<Longrightarrow> sets (K a) = sets N) \<Longrightarrow>
+  (\<And>A. A \<in> sets N \<Longrightarrow> (\<lambda>a. emeasure (K a) A) \<in> borel_measurable M) \<Longrightarrow>
+  K \<in> measurable M (subprob_algebra N)"
+  by (auto intro!: measurable_Sup_sigma2 measurable_vimage_algebra2 simp: subprob_algebra_def)
+
+lemma space_subprob_algebra_empty_iff:
+  "space (subprob_algebra N) = {} \<longleftrightarrow> space N = {}"
+proof
+  have "\<And>x. x \<in> space N \<Longrightarrow> density N (\<lambda>_. 0) \<in> space (subprob_algebra N)"
+    by (auto simp: space_subprob_algebra emeasure_density intro!: subprob_spaceI)
+  then show "space (subprob_algebra N) = {} \<Longrightarrow> space N = {}"
+    by auto
+next
+  assume "space N = {}"
+  hence "sets N = {{}}" by (simp add: space_empty_iff)
+  moreover have "\<And>M. subprob_space M \<Longrightarrow> sets M \<noteq> {{}}"
+    by (simp add: subprob_space.subprob_not_empty space_empty_iff[symmetric])
+  ultimately show "space (subprob_algebra N) = {}" by (auto simp: space_subprob_algebra)
+qed
+
+lemma measurable_distr:
+  assumes [measurable]: "f \<in> measurable M N"
+  shows "(\<lambda>M'. distr M' N f) \<in> measurable (subprob_algebra M) (subprob_algebra N)"
+proof (cases "space N = {}")
+  assume not_empty: "space N \<noteq> {}"
+  show ?thesis
+  proof (rule measurable_subprob_algebra)
+    fix A assume A: "A \<in> sets N"
+    then have "(\<lambda>M'. emeasure (distr M' N f) A) \<in> borel_measurable (subprob_algebra M) \<longleftrightarrow>
+      (\<lambda>M'. emeasure M' (f -` A \<inter> space M)) \<in> borel_measurable (subprob_algebra M)"
+      by (intro measurable_cong)
+         (auto simp: emeasure_distr space_subprob_algebra dest: sets_eq_imp_space_eq cong: measurable_cong)
+    also have "\<dots>"
+      using A by (intro measurable_emeasure_subprob_algebra) simp
+    finally show "(\<lambda>M'. emeasure (distr M' N f) A) \<in> borel_measurable (subprob_algebra M)" .
+  qed (auto intro!: subprob_space.subprob_space_distr simp: space_subprob_algebra not_empty)
+qed (insert assms, auto simp: measurable_empty_iff space_subprob_algebra_empty_iff)
+
+section {* Properties of return *}
+
+definition return :: "'a measure \<Rightarrow> 'a \<Rightarrow> 'a measure" where
+  "return R x = measure_of (space R) (sets R) (\<lambda>A. indicator A x)"
+
+lemma space_return[simp]: "space (return M x) = space M"
+  by (simp add: return_def)
+
+lemma sets_return[simp]: "sets (return M x) = sets M"
+  by (simp add: return_def)
+
+lemma measurable_return1[simp]: "measurable (return N x) L = measurable N L"
+  by (simp cong: measurable_cong_sets) 
+
+lemma measurable_return2[simp]: "measurable L (return N x) = measurable L N"
+  by (simp cong: measurable_cong_sets) 
+
+lemma emeasure_return[simp]:
+  assumes "A \<in> sets M"
+  shows "emeasure (return M x) A = indicator A x"
+proof (rule emeasure_measure_of[OF return_def])
+  show "sets M \<subseteq> Pow (space M)" by (rule sets.space_closed)
+  show "positive (sets (return M x)) (\<lambda>A. indicator A x)" by (simp add: positive_def)
+  from assms show "A \<in> sets (return M x)" unfolding return_def by simp
+  show "countably_additive (sets (return M x)) (\<lambda>A. indicator A x)"
+    by (auto intro: countably_additiveI simp: suminf_indicator)
+qed
+
+lemma prob_space_return: "x \<in> space M \<Longrightarrow> prob_space (return M x)"
+  by rule simp
+
+lemma subprob_space_return: "x \<in> space M \<Longrightarrow> subprob_space (return M x)"
+  by (intro prob_space_return prob_space_imp_subprob_space)
+
+lemma AE_return:
+  assumes [simp]: "x \<in> space M" and [measurable]: "Measurable.pred M P"
+  shows "(AE y in return M x. P y) \<longleftrightarrow> P x"
+proof -
+  have "(AE y in return M x. y \<notin> {x\<in>space M. \<not> P x}) \<longleftrightarrow> P x"
+    by (subst AE_iff_null_sets[symmetric]) (simp_all add: null_sets_def split: split_indicator)
+  also have "(AE y in return M x. y \<notin> {x\<in>space M. \<not> P x}) \<longleftrightarrow> (AE y in return M x. P y)"
+    by (rule AE_cong) auto
+  finally show ?thesis .
+qed
+  
+lemma nn_integral_return:
+  assumes "g x \<ge> 0" "x \<in> space M" "g \<in> borel_measurable M"
+  shows "(\<integral>\<^sup>+ a. g a \<partial>return M x) = g x"
+proof-
+  interpret prob_space "return M x" by (rule prob_space_return[OF `x \<in> space M`])
+  have "(\<integral>\<^sup>+ a. g a \<partial>return M x) = (\<integral>\<^sup>+ a. g x \<partial>return M x)" using assms
+    by (intro nn_integral_cong_AE) (auto simp: AE_return)
+  also have "... = g x"
+    using nn_integral_const[OF `g x \<ge> 0`, of "return M x"] emeasure_space_1 by simp
+  finally show ?thesis .
+qed
+
+lemma return_measurable: "return N \<in> measurable N (subprob_algebra N)"
+  by (rule measurable_subprob_algebra) (auto simp: subprob_space_return)
+
+lemma distr_return:
+  assumes "f \<in> measurable M N" and "x \<in> space M"
+  shows "distr (return M x) N f = return N (f x)"
+  using assms by (intro measure_eqI) (simp_all add: indicator_def emeasure_distr)
+
+definition "select_sets M = (SOME N. sets M = sets (subprob_algebra N))"
+
+lemma select_sets1:
+  "sets M = sets (subprob_algebra N) \<Longrightarrow> sets M = sets (subprob_algebra (select_sets M))"
+  unfolding select_sets_def by (rule someI)
+
+lemma sets_select_sets[simp]:
+  assumes sets: "sets M = sets (subprob_algebra N)"
+  shows "sets (select_sets M) = sets N"
+  unfolding select_sets_def
+proof (rule someI2)
+  show "sets M = sets (subprob_algebra N)"
+    by fact
+next
+  fix L assume "sets M = sets (subprob_algebra L)"
+  with sets have eq: "space (subprob_algebra N) = space (subprob_algebra L)"
+    by (intro sets_eq_imp_space_eq) simp
+  show "sets L = sets N"
+  proof cases
+    assume "space (subprob_algebra N) = {}"
+    with space_subprob_algebra_empty_iff[of N] space_subprob_algebra_empty_iff[of L]
+    show ?thesis
+      by (simp add: eq space_empty_iff)
+  next
+    assume "space (subprob_algebra N) \<noteq> {}"
+    with eq show ?thesis
+      by (fastforce simp add: space_subprob_algebra)
+  qed
+qed
+
+lemma space_select_sets[simp]:
+  "sets M = sets (subprob_algebra N) \<Longrightarrow> space (select_sets M) = space N"
+  by (intro sets_eq_imp_space_eq sets_select_sets)
+
+section {* Join *}
+
+definition join :: "'a measure measure \<Rightarrow> 'a measure" where
+  "join M = measure_of (space (select_sets M)) (sets (select_sets M)) (\<lambda>B. \<integral>\<^sup>+ M'. emeasure M' B \<partial>M)"
+
+lemma
+  shows space_join[simp]: "space (join M) = space (select_sets M)"
+    and sets_join[simp]: "sets (join M) = sets (select_sets M)"
+  by (simp_all add: join_def)
+
+lemma emeasure_join:
+  assumes M[simp]: "sets M = sets (subprob_algebra N)" and A: "A \<in> sets N"
+  shows "emeasure (join M) A = (\<integral>\<^sup>+ M'. emeasure M' A \<partial>M)"
+proof (rule emeasure_measure_of[OF join_def])
+  have eq: "borel_measurable M = borel_measurable (subprob_algebra N)"
+    by auto
+  show "countably_additive (sets (join M)) (\<lambda>B. \<integral>\<^sup>+ M'. emeasure M' B \<partial>M)"
+  proof (rule countably_additiveI)
+    fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets (join M)" "disjoint_family A"
+    have "(\<Sum>i. \<integral>\<^sup>+ M'. emeasure M' (A i) \<partial>M) = (\<integral>\<^sup>+M'. (\<Sum>i. emeasure M' (A i)) \<partial>M)"
+      using A by (subst nn_integral_suminf) (auto simp: measurable_emeasure_subprob_algebra eq)
+    also have "\<dots> = (\<integral>\<^sup>+M'. emeasure M' (\<Union>i. A i) \<partial>M)"
+    proof (rule nn_integral_cong)
+      fix M' assume "M' \<in> space M"
+      then show "(\<Sum>i. emeasure M' (A i)) = emeasure M' (\<Union>i. A i)"
+        using A sets_eq_imp_space_eq[OF M] by (simp add: suminf_emeasure space_subprob_algebra)
+    qed
+    finally show "(\<Sum>i. \<integral>\<^sup>+M'. emeasure M' (A i) \<partial>M) = (\<integral>\<^sup>+M'. emeasure M' (\<Union>i. A i) \<partial>M)" .
+  qed
+qed (auto simp: A sets.space_closed positive_def nn_integral_nonneg)
+
+lemma nn_integral_measurable_subprob_algebra:
+  assumes f: "f \<in> borel_measurable N" "\<And>x. 0 \<le> f x"
+  shows "(\<lambda>M. integral\<^sup>N M f) \<in> borel_measurable (subprob_algebra N)" (is "_ \<in> ?B")
+  using f
+proof induct
+  case (cong f g)
+  moreover have "(\<lambda>M'. \<integral>\<^sup>+M''. f M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. \<integral>\<^sup>+M''. g M'' \<partial>M') \<in> ?B"
+    by (intro measurable_cong nn_integral_cong cong)
+       (auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq)
+  ultimately show ?case by simp
+next
+  case (set B)
+  moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. indicator B M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. emeasure M' B) \<in> ?B"
+    by (intro measurable_cong nn_integral_indicator) (simp add: space_subprob_algebra)
+  ultimately show ?case
+    by (simp add: measurable_emeasure_subprob_algebra)
+next
+  case (mult f c)
+  moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. c * f M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. c * \<integral>\<^sup>+M''. f M'' \<partial>M') \<in> ?B"
+    by (intro measurable_cong nn_integral_cmult) (simp add: space_subprob_algebra)
+  ultimately show ?case
+    by simp
+next
+  case (add f g)
+  moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. f M'' + g M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. (\<integral>\<^sup>+M''. f M'' \<partial>M') + (\<integral>\<^sup>+M''. g M'' \<partial>M')) \<in> ?B"
+    by (intro measurable_cong nn_integral_add) (simp_all add: space_subprob_algebra)
+  ultimately show ?case
+    by (simp add: ac_simps)
+next
+  case (seq F)
+  moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. (SUP i. F i) M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. SUP i. (\<integral>\<^sup>+M''. F i M'' \<partial>M')) \<in> ?B"
+    unfolding SUP_apply
+    by (intro measurable_cong nn_integral_monotone_convergence_SUP) (simp_all add: space_subprob_algebra)
+  ultimately show ?case
+    by (simp add: ac_simps)
+qed
+
+
+lemma measurable_join:
+  "join \<in> measurable (subprob_algebra (subprob_algebra N)) (subprob_algebra N)"
+proof (cases "space N \<noteq> {}", rule measurable_subprob_algebra)
+  fix A assume "A \<in> sets N"
+  let ?B = "borel_measurable (subprob_algebra (subprob_algebra N))"
+  have "(\<lambda>M'. emeasure (join M') A) \<in> ?B \<longleftrightarrow> (\<lambda>M'. (\<integral>\<^sup>+ M''. emeasure M'' A \<partial>M')) \<in> ?B"
+  proof (rule measurable_cong)
+    fix M' assume "M' \<in> space (subprob_algebra (subprob_algebra N))"
+    then show "emeasure (join M') A = (\<integral>\<^sup>+ M''. emeasure M'' A \<partial>M')"
+      by (intro emeasure_join) (auto simp: space_subprob_algebra `A\<in>sets N`)
+  qed
+  also have "(\<lambda>M'. \<integral>\<^sup>+M''. emeasure M'' A \<partial>M') \<in> ?B"
+    using measurable_emeasure_subprob_algebra[OF `A\<in>sets N`] emeasure_nonneg[of _ A]
+    by (rule nn_integral_measurable_subprob_algebra)
+  finally show "(\<lambda>M'. emeasure (join M') A) \<in> borel_measurable (subprob_algebra (subprob_algebra N))" .
+next
+  assume [simp]: "space N \<noteq> {}"
+  fix M assume M: "M \<in> space (subprob_algebra (subprob_algebra N))"
+  then have "(\<integral>\<^sup>+M'. emeasure M' (space N) \<partial>M) \<le> (\<integral>\<^sup>+M'. 1 \<partial>M)"
+    apply (intro nn_integral_mono)
+    apply (auto simp: space_subprob_algebra 
+                 dest!: sets_eq_imp_space_eq subprob_space.emeasure_space_le_1)
+    done
+  with M show "subprob_space (join M)"
+    by (intro subprob_spaceI)
+       (auto simp: emeasure_join space_subprob_algebra M assms dest: subprob_space.emeasure_space_le_1)
+next
+  assume "\<not>(space N \<noteq> {})"
+  thus ?thesis by (simp add: measurable_empty_iff space_subprob_algebra_empty_iff)
+qed (auto simp: space_subprob_algebra)
+
+lemma nn_integral_join:
+  assumes f: "f \<in> borel_measurable N" "\<And>x. 0 \<le> f x" and M: "sets M = sets (subprob_algebra N)"
+  shows "(\<integral>\<^sup>+x. f x \<partial>join M) = (\<integral>\<^sup>+M'. \<integral>\<^sup>+x. f x \<partial>M' \<partial>M)"
+  using f
+proof induct
+  case (cong f g)
+  moreover have "integral\<^sup>N (join M) f = integral\<^sup>N (join M) g"
+    by (intro nn_integral_cong cong) (simp add: M)
+  moreover from M have "(\<integral>\<^sup>+ M'. integral\<^sup>N M' f \<partial>M) = (\<integral>\<^sup>+ M'. integral\<^sup>N M' g \<partial>M)"
+    by (intro nn_integral_cong cong)
+       (auto simp add: space_subprob_algebra dest!: sets_eq_imp_space_eq)
+  ultimately show ?case
+    by simp
+next
+  case (set A)
+  moreover with M have "(\<integral>\<^sup>+ M'. integral\<^sup>N M' (indicator A) \<partial>M) = (\<integral>\<^sup>+ M'. emeasure M' A \<partial>M)" 
+    by (intro nn_integral_cong nn_integral_indicator)
+       (auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq)
+  ultimately show ?case
+    using M by (simp add: emeasure_join)
+next
+  case (mult f c)
+  have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. c * f x \<partial>M' \<partial>M) = (\<integral>\<^sup>+ M'. c * \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)"
+    using mult M
+    by (intro nn_integral_cong nn_integral_cmult)
+       (auto simp add: space_subprob_algebra cong: measurable_cong dest!: sets_eq_imp_space_eq)
+  also have "\<dots> = c * (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)"
+    using nn_integral_measurable_subprob_algebra[OF mult(3,4)]
+    by (intro nn_integral_cmult mult) (simp add: M)
+  also have "\<dots> = c * (integral\<^sup>N (join M) f)"
+    by (simp add: mult)
+  also have "\<dots> = (\<integral>\<^sup>+ x. c * f x \<partial>join M)"
+    using mult(2,3) by (intro nn_integral_cmult[symmetric] mult) (simp add: M)
+  finally show ?case by simp
+next
+  case (add f g)
+  have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x + g x \<partial>M' \<partial>M) = (\<integral>\<^sup>+ M'. (\<integral>\<^sup>+ x. f x \<partial>M') + (\<integral>\<^sup>+ x. g x \<partial>M') \<partial>M)"
+    using add M
+    by (intro nn_integral_cong nn_integral_add)
+       (auto simp add: space_subprob_algebra cong: measurable_cong dest!: sets_eq_imp_space_eq)
+  also have "\<dots> = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M) + (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. g x \<partial>M' \<partial>M)"
+    using nn_integral_measurable_subprob_algebra[OF add(1,2)]
+    using nn_integral_measurable_subprob_algebra[OF add(5,6)]
+    by (intro nn_integral_add add) (simp_all add: M nn_integral_nonneg)
+  also have "\<dots> = (integral\<^sup>N (join M) f) + (integral\<^sup>N (join M) g)"
+    by (simp add: add)
+  also have "\<dots> = (\<integral>\<^sup>+ x. f x + g x \<partial>join M)"
+    using add by (intro nn_integral_add[symmetric] add) (simp_all add: M)
+  finally show ?case by (simp add: ac_simps)
+next
+  case (seq F)
+  have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. (SUP i. F i) x \<partial>M' \<partial>M) = (\<integral>\<^sup>+ M'. (SUP i. \<integral>\<^sup>+ x. F i x \<partial>M') \<partial>M)"
+    using seq M unfolding SUP_apply
+    by (intro nn_integral_cong nn_integral_monotone_convergence_SUP)
+       (auto simp add: space_subprob_algebra cong: measurable_cong dest!: sets_eq_imp_space_eq)
+  also have "\<dots> = (SUP i. \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. F i x \<partial>M' \<partial>M)"
+    using nn_integral_measurable_subprob_algebra[OF seq(1,2)] seq
+    by (intro nn_integral_monotone_convergence_SUP)
+       (simp_all add: M nn_integral_nonneg incseq_nn_integral incseq_def le_fun_def nn_integral_mono )
+  also have "\<dots> = (SUP i. integral\<^sup>N (join M) (F i))"
+    by (simp add: seq)
+  also have "\<dots> = (\<integral>\<^sup>+ x. (SUP i. F i x) \<partial>join M)"
+    using seq by (intro nn_integral_monotone_convergence_SUP[symmetric] seq) (simp_all add: M)
+  finally show ?case by (simp add: ac_simps)
+qed
+
+lemma join_assoc:
+  assumes M: "sets M = sets (subprob_algebra (subprob_algebra N))"
+  shows "join (distr M (subprob_algebra N) join) = join (join M)"
+proof (rule measure_eqI)
+  fix A assume "A \<in> sets (join (distr M (subprob_algebra N) join))"
+  then have A: "A \<in> sets N" by simp
+  show "emeasure (join (distr M (subprob_algebra N) join)) A = emeasure (join (join M)) A"
+    using measurable_join[of N]
+    by (auto simp: M A nn_integral_distr emeasure_join measurable_emeasure_subprob_algebra emeasure_nonneg
+                   sets_eq_imp_space_eq[OF M] space_subprob_algebra nn_integral_join[OF _ _ M]
+             intro!: nn_integral_cong emeasure_join cong: measurable_cong)
+qed (simp add: M)
+
+lemma join_return: 
+  assumes "sets M = sets N" and "subprob_space M"
+  shows "join (return (subprob_algebra N) M) = M"
+  by (rule measure_eqI)
+     (simp_all add: emeasure_join emeasure_nonneg space_subprob_algebra  
+                    measurable_emeasure_subprob_algebra nn_integral_return assms)
+
+lemma join_return':
+  assumes "sets N = sets M"
+  shows "join (distr M (subprob_algebra N) (return N)) = M"
+apply (rule measure_eqI)
+apply (simp add: assms)
+apply (subgoal_tac "return N \<in> measurable M (subprob_algebra N)")
+apply (simp add: emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra assms)
+apply (subst measurable_cong_sets, rule assms[symmetric], rule refl, rule return_measurable)
+done
+
+lemma join_distr_distr:
+  fixes f :: "'a \<Rightarrow> 'b" and M :: "'a measure measure" and N :: "'b measure"
+  assumes "sets M = sets (subprob_algebra R)" and "f \<in> measurable R N"
+  shows "join (distr M (subprob_algebra N) (\<lambda>M. distr M N f)) = distr (join M) N f" (is "?r = ?l")
+proof (rule measure_eqI)
+  fix A assume "A \<in> sets ?r"
+  hence A_in_N: "A \<in> sets N" by simp
+
+  from assms have "f \<in> measurable (join M) N" 
+      by (simp cong: measurable_cong_sets)
+  moreover from assms and A_in_N have "f-`A \<inter> space R \<in> sets R" 
+      by (intro measurable_sets) simp_all
+  ultimately have "emeasure (distr (join M) N f) A = \<integral>\<^sup>+M'. emeasure M' (f-`A \<inter> space R) \<partial>M"
+      by (simp_all add: A_in_N emeasure_distr emeasure_join assms)
+  
+  also have "... = \<integral>\<^sup>+ x. emeasure (distr x N f) A \<partial>M" using A_in_N
+  proof (intro nn_integral_cong, subst emeasure_distr)
+    fix M' assume "M' \<in> space M"
+    from assms have "space M = space (subprob_algebra R)"
+        using sets_eq_imp_space_eq by blast
+    with `M' \<in> space M` have [simp]: "sets M' = sets R" using space_subprob_algebra by blast
+    show "f \<in> measurable M' N" by (simp cong: measurable_cong_sets add: assms)
+    have "space M' = space R" by (rule sets_eq_imp_space_eq) simp
+    thus "emeasure M' (f -` A \<inter> space R) = emeasure M' (f -` A \<inter> space M')" by simp
+  qed
+
+  also have "(\<lambda>M. distr M N f) \<in> measurable M (subprob_algebra N)"
+      by (simp cong: measurable_cong_sets add: assms measurable_distr)
+  hence "(\<integral>\<^sup>+ x. emeasure (distr x N f) A \<partial>M) = 
+             emeasure (join (distr M (subprob_algebra N) (\<lambda>M. distr M N f))) A"
+      by (simp_all add: emeasure_join assms A_in_N nn_integral_distr measurable_emeasure_subprob_algebra)
+  finally show "emeasure ?r A = emeasure ?l A" ..
+qed simp
+
+definition bind :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b measure) \<Rightarrow> 'b measure" where
+  "bind M f = (if space M = {} then count_space {} else
+    join (distr M (subprob_algebra (f (SOME x. x \<in> space M))) f))"
+
+adhoc_overloading Monad_Syntax.bind bind
+
+lemma bind_empty: 
+  "space M = {} \<Longrightarrow> bind M f = count_space {}"
+  by (simp add: bind_def)
+
+lemma bind_nonempty:
+  "space M \<noteq> {} \<Longrightarrow> bind M f = join (distr M (subprob_algebra (f (SOME x. x \<in> space M))) f)"
+  by (simp add: bind_def)
+
+lemma sets_bind_empty: "sets M = {} \<Longrightarrow> sets (bind M f) = {{}}"
+  by (auto simp: bind_def)
+
+lemma space_bind_empty: "space M = {} \<Longrightarrow> space (bind M f) = {}"
+  by (simp add: bind_def)
+
+lemma sets_bind[simp]: 
+  assumes "f \<in> measurable M (subprob_algebra N)" and "space M \<noteq> {}"
+  shows "sets (bind M f) = sets N"
+    using assms(2) by (force simp: bind_nonempty intro!: sets_kernel[OF assms(1) someI_ex])
+
+lemma space_bind[simp]: 
+  assumes "f \<in> measurable M (subprob_algebra N)" and "space M \<noteq> {}"
+  shows "space (bind M f) = space N"
+    using assms by (intro sets_eq_imp_space_eq sets_bind)
+
+lemma bind_cong: 
+  assumes "\<forall>x \<in> space M. f x = g x"
+  shows "bind M f = bind M g"
+proof (cases "space M = {}")
+  assume "space M \<noteq> {}"
+  hence "(SOME x. x \<in> space M) \<in> space M" by (rule_tac someI_ex) blast
+  with assms have "f (SOME x. x \<in> space M) = g (SOME x. x \<in> space M)" by blast
+  with `space M \<noteq> {}` and assms show ?thesis by (simp add: bind_nonempty cong: distr_cong)
+qed (simp add: bind_empty)
+
+lemma bind_nonempty':
+  assumes "f \<in> measurable M (subprob_algebra N)" "x \<in> space M"
+  shows "bind M f = join (distr M (subprob_algebra N) f)"
+  using assms
+  apply (subst bind_nonempty, blast)
+  apply (subst subprob_algebra_cong[OF sets_kernel[OF assms(1) someI_ex]], blast)
+  apply (simp add: subprob_algebra_cong[OF sets_kernel[OF assms]])
+  done
+
+lemma bind_nonempty'':
+  assumes "f \<in> measurable M (subprob_algebra N)" "space M \<noteq> {}"
+  shows "bind M f = join (distr M (subprob_algebra N) f)"
+  using assms by (auto intro: bind_nonempty')
+
+lemma emeasure_bind:
+    "\<lbrakk>space M \<noteq> {}; f \<in> measurable M (subprob_algebra N);X \<in> sets N\<rbrakk>
+      \<Longrightarrow> emeasure (M \<guillemotright>= f) X = \<integral>\<^sup>+x. emeasure (f x) X \<partial>M"
+  by (simp add: bind_nonempty'' emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra)
+
+lemma bind_return: 
+  assumes "f \<in> measurable M (subprob_algebra N)" and "x \<in> space M"
+  shows "bind (return M x) f = f x"
+  using sets_kernel[OF assms] assms
+  by (simp_all add: distr_return join_return subprob_space_kernel bind_nonempty'
+               cong: subprob_algebra_cong)
+
+lemma bind_return':
+  shows "bind M (return M) = M"
+  by (cases "space M = {}")
+     (simp_all add: bind_empty space_empty[symmetric] bind_nonempty join_return' 
+               cong: subprob_algebra_cong)
+
+lemma bind_count_space_singleton:
+  assumes "subprob_space (f x)"
+  shows "count_space {x} \<guillemotright>= f = f x"
+proof-
+  have A: "\<And>A. A \<subseteq> {x} \<Longrightarrow> A = {} \<or> A = {x}" by auto
+  have "count_space {x} = return (count_space {x}) x"
+    by (intro measure_eqI) (auto dest: A)
+  also have "... \<guillemotright>= f = f x"
+    by (subst bind_return[of _ _ "f x"]) (auto simp: space_subprob_algebra assms)
+  finally show ?thesis .
+qed
+
+lemma emeasure_bind_const: 
+    "space M \<noteq> {} \<Longrightarrow> X \<in> sets N \<Longrightarrow> subprob_space N \<Longrightarrow> 
+         emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)"
+  by (simp add: bind_nonempty emeasure_join nn_integral_distr 
+                space_subprob_algebra measurable_emeasure_subprob_algebra emeasure_nonneg)
+
+lemma emeasure_bind_const':
+  assumes "subprob_space M" "subprob_space N"
+  shows "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)"
+using assms
+proof (case_tac "X \<in> sets N")
+  fix X assume "X \<in> sets N"
+  thus "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)" using assms
+      by (subst emeasure_bind_const) 
+         (simp_all add: subprob_space.subprob_not_empty subprob_space.emeasure_space_le_1)
+next
+  fix X assume "X \<notin> sets N"
+  with assms show "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)"
+      by (simp add: sets_bind[of _ _ N] subprob_space.subprob_not_empty
+                    space_subprob_algebra emeasure_notin_sets)
+qed
+
+lemma emeasure_bind_const_prob_space:
+  assumes "prob_space M" "subprob_space N"
+  shows "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X"
+  using assms by (simp add: emeasure_bind_const' prob_space_imp_subprob_space 
+                            prob_space.emeasure_space_1)
+
+lemma bind_const': "\<lbrakk>prob_space M; subprob_space N\<rbrakk> \<Longrightarrow> M \<guillemotright>= (\<lambda>x. N) = N"
+  by (intro measure_eqI) 
+     (simp_all add: space_subprob_algebra prob_space.not_empty emeasure_bind_const_prob_space)
+
+lemma bind_return_distr: 
+    "space M \<noteq> {} \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> bind M (return N \<circ> f) = distr M N f"
+  apply (simp add: bind_nonempty)
+  apply (subst subprob_algebra_cong)
+  apply (rule sets_return)
+  apply (subst distr_distr[symmetric])
+  apply (auto intro!: return_measurable simp: distr_distr[symmetric] join_return')
+  done
+
+lemma bind_assoc:
+  fixes f :: "'a \<Rightarrow> 'b measure" and g :: "'b \<Rightarrow> 'c measure"
+  assumes M1: "f \<in> measurable M (subprob_algebra N)" and M2: "g \<in> measurable N (subprob_algebra R)"
+  shows "bind (bind M f) g = bind M (\<lambda>x. bind (f x) g)"
+proof (cases "space M = {}")
+  assume [simp]: "space M \<noteq> {}"
+  from assms have [simp]: "space N \<noteq> {}" "space R \<noteq> {}"
+      by (auto simp: measurable_empty_iff space_subprob_algebra_empty_iff)
+  from assms have sets_fx[simp]: "\<And>x. x \<in> space M \<Longrightarrow> sets (f x) = sets N"
+      by (simp add: sets_kernel)
+  have ex_in: "\<And>A. A \<noteq> {} \<Longrightarrow> \<exists>x. x \<in> A" by blast
+  note sets_some[simp] = sets_kernel[OF M1 someI_ex[OF ex_in[OF `space M \<noteq> {}`]]]
+                         sets_kernel[OF M2 someI_ex[OF ex_in[OF `space N \<noteq> {}`]]]
+  note space_some[simp] = sets_eq_imp_space_eq[OF this(1)] sets_eq_imp_space_eq[OF this(2)]
+
+  have "bind M (\<lambda>x. bind (f x) g) = 
+        join (distr M (subprob_algebra R) (join \<circ> (\<lambda>x. (distr x (subprob_algebra R) g)) \<circ> f))"
+    by (simp add: sets_eq_imp_space_eq[OF sets_fx] bind_nonempty o_def
+             cong: subprob_algebra_cong distr_cong)
+  also have "distr M (subprob_algebra R) (join \<circ> (\<lambda>x. (distr x (subprob_algebra R) g)) \<circ> f) =
+             distr (distr (distr M (subprob_algebra N) f)
+                          (subprob_algebra (subprob_algebra R))
+                          (\<lambda>x. distr x (subprob_algebra R) g)) 
+                   (subprob_algebra R) join"
+      apply (subst distr_distr, 
+             (blast intro: measurable_comp measurable_distr measurable_join M1 M2)+)+
+      apply (simp add: o_assoc)
+      done
+  also have "join ... = bind (bind M f) g"
+      by (simp add: join_assoc join_distr_distr M2 bind_nonempty cong: subprob_algebra_cong)
+  finally show ?thesis ..
+qed (simp add: bind_empty)
+
+lemma emeasure_space_subprob_algebra[measurable]:
+  "(\<lambda>a. emeasure a (space a)) \<in> borel_measurable (subprob_algebra N)"
+proof-
+  have "(\<lambda>a. emeasure a (space N)) \<in> borel_measurable (subprob_algebra N)" (is "?f \<in> ?M")
+    by (rule measurable_emeasure_subprob_algebra) simp
+  also have "?f \<in> ?M \<longleftrightarrow> (\<lambda>a. emeasure a (space a)) \<in> ?M"
+    by (rule measurable_cong) (auto simp: space_subprob_algebra dest: sets_eq_imp_space_eq)
+  finally show ?thesis .
+qed
+
+(* TODO: Rename. This name is too general – Manuel *)
+lemma measurable_pair_measure:
+  assumes f: "f \<in> measurable M (subprob_algebra N)"
+  assumes g: "g \<in> measurable M (subprob_algebra L)"
+  shows "(\<lambda>x. f x \<Otimes>\<^sub>M g x) \<in> measurable M (subprob_algebra (N \<Otimes>\<^sub>M L))"
+proof (rule measurable_subprob_algebra)
+  { fix x assume "x \<in> space M"
+    with measurable_space[OF f] measurable_space[OF g]
+    have fx: "f x \<in> space (subprob_algebra N)" and gx: "g x \<in> space (subprob_algebra L)"
+      by auto
+    interpret F: subprob_space "f x"
+      using fx by (simp add: space_subprob_algebra)
+    interpret G: subprob_space "g x"
+      using gx by (simp add: space_subprob_algebra)
+
+    interpret pair_subprob_space "f x" "g x" ..
+    show "subprob_space (f x \<Otimes>\<^sub>M g x)" by unfold_locales
+    show sets_eq: "sets (f x \<Otimes>\<^sub>M g x) = sets (N \<Otimes>\<^sub>M L)"
+      using fx gx by (simp add: space_subprob_algebra)
+
+    have 1: "\<And>A B. A \<in> sets N \<Longrightarrow> B \<in> sets L \<Longrightarrow> emeasure (f x \<Otimes>\<^sub>M g x) (A \<times> B) = emeasure (f x) A * emeasure (g x) B"
+      using fx gx by (intro G.emeasure_pair_measure_Times) (auto simp: space_subprob_algebra) 
+    have "emeasure (f x \<Otimes>\<^sub>M g x) (space (f x \<Otimes>\<^sub>M g x)) = 
+              emeasure (f x) (space (f x)) * emeasure (g x) (space (g x))"
+      by (subst G.emeasure_pair_measure_Times[symmetric]) (simp_all add: space_pair_measure)
+    hence 2: "\<And>A. A \<in> sets (N \<Otimes>\<^sub>M L) \<Longrightarrow> emeasure (f x \<Otimes>\<^sub>M g x) (space N \<times> space L - A) =
+                                             ... - emeasure (f x \<Otimes>\<^sub>M g x) A"
+      using emeasure_compl[OF _ P.emeasure_finite]
+      unfolding sets_eq
+      unfolding sets_eq_imp_space_eq[OF sets_eq]
+      by (simp add: space_pair_measure G.emeasure_pair_measure_Times)
+    note 1 2 sets_eq }
+  note Times = this(1) and Compl = this(2) and sets_eq = this(3)
+
+  fix A assume A: "A \<in> sets (N \<Otimes>\<^sub>M L)"
+  show "(\<lambda>a. emeasure (f a \<Otimes>\<^sub>M g a) A) \<in> borel_measurable M"
+    using Int_stable_pair_measure_generator pair_measure_closed A
+    unfolding sets_pair_measure
+  proof (induct A rule: sigma_sets_induct_disjoint)
+    case (basic A) then show ?case
+      by (auto intro!: borel_measurable_ereal_times simp: Times cong: measurable_cong)
+         (auto intro!: measurable_emeasure_kernel f g)
+  next
+    case (compl A)
+    then have A: "A \<in> sets (N \<Otimes>\<^sub>M L)"
+      by (auto simp: sets_pair_measure)
+    have "(\<lambda>x. emeasure (f x) (space (f x)) * emeasure (g x) (space (g x)) - 
+                   emeasure (f x \<Otimes>\<^sub>M g x) A) \<in> borel_measurable M" (is "?f \<in> ?M")
+      using compl(2) f g by measurable
+    thus ?case by (simp add: Compl A cong: measurable_cong)
+  next
+    case (union A)
+    then have "range A \<subseteq> sets (N \<Otimes>\<^sub>M L)" "disjoint_family A"
+      by (auto simp: sets_pair_measure)
+    then have "(\<lambda>a. emeasure (f a \<Otimes>\<^sub>M g a) (\<Union>i. A i)) \<in> borel_measurable M \<longleftrightarrow>
+      (\<lambda>a. \<Sum>i. emeasure (f a \<Otimes>\<^sub>M g a) (A i)) \<in> borel_measurable M"
+      by (intro measurable_cong suminf_emeasure[symmetric])
+         (auto simp: sets_eq)
+    also have "\<dots>"
+      using union by auto
+    finally show ?case .
+  qed simp
+qed
+
+(* TODO: Move *)
+lemma measurable_distr2:
+  assumes f[measurable]: "split f \<in> measurable (L \<Otimes>\<^sub>M M) N"
+  assumes g[measurable]: "g \<in> measurable L (subprob_algebra M)"
+  shows "(\<lambda>x. distr (g x) N (f x)) \<in> measurable L (subprob_algebra N)"
+proof -
+  have "(\<lambda>x. distr (g x) N (f x)) \<in> measurable L (subprob_algebra N)
+    \<longleftrightarrow> (\<lambda>x. distr (return L x \<Otimes>\<^sub>M g x) N (split f)) \<in> measurable L (subprob_algebra N)"
+  proof (rule measurable_cong)
+    fix x assume x: "x \<in> space L"
+    have gx: "g x \<in> space (subprob_algebra M)"
+      using measurable_space[OF g x] .
+    then have [simp]: "sets (g x) = sets M"
+      by (simp add: space_subprob_algebra)
+    then have [simp]: "space (g x) = space M"
+      by (rule sets_eq_imp_space_eq)
+    let ?R = "return L x"
+    from measurable_compose_Pair1[OF x f] have f_M': "f x \<in> measurable M N"
+      by simp
+    interpret subprob_space "g x"
+      using gx by (simp add: space_subprob_algebra)
+    have space_pair_M'[simp]: "\<And>X. space (X \<Otimes>\<^sub>M g x) = space (X \<Otimes>\<^sub>M M)"
+      by (simp add: space_pair_measure)
+    show "distr (g x) N (f x) = distr (?R \<Otimes>\<^sub>M g x) N (split f)" (is "?l = ?r")
+    proof (rule measure_eqI)
+      show "sets ?l = sets ?r"
+        by simp
+    next
+      fix A assume "A \<in> sets ?l"
+      then have A[measurable]: "A \<in> sets N"
+        by simp
+      then have "emeasure ?r A = emeasure (?R \<Otimes>\<^sub>M g x) ((\<lambda>(x, y). f x y) -` A \<inter> space (?R \<Otimes>\<^sub>M g x))"
+        by (auto simp add: emeasure_distr f_M' cong: measurable_cong_sets)
+      also have "\<dots> = (\<integral>\<^sup>+M''. emeasure (g x) (f M'' -` A \<inter> space M) \<partial>?R)"
+        apply (subst emeasure_pair_measure_alt)
+        apply (rule measurable_sets[OF _ A])
+        apply (auto simp add: f_M' cong: measurable_cong_sets)
+        apply (intro nn_integral_cong arg_cong[where f="emeasure (g x)"])
+        apply (auto simp: space_subprob_algebra space_pair_measure)
+        done
+      also have "\<dots> = emeasure (g x) (f x -` A \<inter> space M)"
+        by (subst nn_integral_return)
+           (auto simp: x intro!: measurable_emeasure)
+      also have "\<dots> = emeasure ?l A"
+        by (simp add: emeasure_distr f_M' cong: measurable_cong_sets)
+      finally show "emeasure ?l A = emeasure ?r A" ..
+    qed
+  qed
+  also have "\<dots>"
+    apply (intro measurable_compose[OF measurable_pair_measure measurable_distr])
+    apply (rule return_measurable)
+    apply measurable
+    done
+  finally show ?thesis .
+qed
+
+(* END TODO *)
+
+lemma measurable_bind':
+  assumes M1: "f \<in> measurable M (subprob_algebra N)" and
+          M2: "split g \<in> measurable (M \<Otimes>\<^sub>M N) (subprob_algebra R)"
+  shows "(\<lambda>x. bind (f x) (g x)) \<in> measurable M (subprob_algebra R)"
+proof (subst measurable_cong)
+  fix x assume x_in_M: "x \<in> space M"
+  with assms have "space (f x) \<noteq> {}" 
+      by (blast dest: subprob_space_kernel subprob_space.subprob_not_empty)
+  moreover from M2 x_in_M have "g x \<in> measurable (f x) (subprob_algebra R)"
+      by (subst measurable_cong_sets[OF sets_kernel[OF M1 x_in_M] refl])
+         (auto dest: measurable_Pair2)
+  ultimately show "bind (f x) (g x) = join (distr (f x) (subprob_algebra R) (g x))" 
+      by (simp_all add: bind_nonempty'')
+next
+  show "(\<lambda>w. join (distr (f w) (subprob_algebra R) (g w))) \<in> measurable M (subprob_algebra R)"
+    apply (rule measurable_compose[OF _ measurable_join])
+    apply (rule measurable_distr2[OF M2 M1])
+    done
+qed
+
+lemma measurable_bind:
+  assumes M1: "f \<in> measurable M (subprob_algebra N)" and
+          M2: "(\<lambda>x. g (fst x) (snd x)) \<in> measurable (M \<Otimes>\<^sub>M N) (subprob_algebra R)"
+  shows "(\<lambda>x. bind (f x) (g x)) \<in> measurable M (subprob_algebra R)"
+  using assms by (auto intro: measurable_bind' simp: measurable_split_conv)
+
+lemma measurable_bind2:
+  assumes "f \<in> measurable M (subprob_algebra N)" and "g \<in> measurable N (subprob_algebra R)"
+  shows "(\<lambda>x. bind (f x) g) \<in> measurable M (subprob_algebra R)"
+    using assms by (intro measurable_bind' measurable_const) auto
+
+lemma subprob_space_bind:
+  assumes "subprob_space M" "f \<in> measurable M (subprob_algebra N)"
+  shows "subprob_space (M \<guillemotright>= f)"
+proof (rule subprob_space_kernel[of "\<lambda>x. x \<guillemotright>= f"])
+  show "(\<lambda>x. x \<guillemotright>= f) \<in> measurable (subprob_algebra M) (subprob_algebra N)"
+    by (rule measurable_bind, rule measurable_ident_sets, rule refl, 
+        rule measurable_compose[OF measurable_snd assms(2)])
+  from assms(1) show "M \<in> space (subprob_algebra M)"
+    by (simp add: space_subprob_algebra)
+qed
+
+lemma double_bind_assoc:
+  assumes Mg: "g \<in> measurable N (subprob_algebra N')"
+  assumes Mf: "f \<in> measurable M (subprob_algebra M')"
+  assumes Mh: "split h \<in> measurable (M \<Otimes>\<^sub>M M') N"
+  shows "do {x \<leftarrow> M; y \<leftarrow> f x; g (h x y)} = do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y)} \<guillemotright>= g"
+proof-
+  have "do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y)} \<guillemotright>= g = 
+            do {x \<leftarrow> M; do {y \<leftarrow> f x; return N (h x y)} \<guillemotright>= g}"
+    using Mh by (auto intro!: bind_assoc measurable_bind'[OF Mf] Mf Mg
+                      measurable_compose[OF _ return_measurable] simp: measurable_split_conv)
+  also from Mh have "\<And>x. x \<in> space M \<Longrightarrow> h x \<in> measurable M' N" by measurable
+  hence "do {x \<leftarrow> M; do {y \<leftarrow> f x; return N (h x y)} \<guillemotright>= g} = 
+            do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y) \<guillemotright>= g}"
+    apply (intro ballI bind_cong bind_assoc)
+    apply (subst measurable_cong_sets[OF sets_kernel[OF Mf] refl], simp)
+    apply (rule measurable_compose[OF _ return_measurable], auto intro: Mg)
+    done
+  also have "\<And>x. x \<in> space M \<Longrightarrow> space (f x) = space M'"
+    by (intro sets_eq_imp_space_eq sets_kernel[OF Mf])
+  with measurable_space[OF Mh] 
+    have "do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y) \<guillemotright>= g} = do {x \<leftarrow> M; y \<leftarrow> f x; g (h x y)}"
+    by (intro ballI bind_cong bind_return[OF Mg]) (auto simp: space_pair_measure)
+  finally show ?thesis ..
+qed
+
+section {* Measures form a $\omega$-chain complete partial order *}
+
+definition SUP_measure :: "(nat \<Rightarrow> 'a measure) \<Rightarrow> 'a measure" where
+  "SUP_measure M = measure_of (\<Union>i. space (M i)) (\<Union>i. sets (M i)) (\<lambda>A. SUP i. emeasure (M i) A)"
+
+lemma
+  assumes const: "\<And>i j. sets (M i) = sets (M j)"
+  shows space_SUP_measure: "space (SUP_measure M) = space (M i)" (is ?sp)
+    and sets_SUP_measure: "sets (SUP_measure M) = sets (M i)" (is ?st)
+proof -
+  have "(\<Union>i. sets (M i)) = sets (M i)"
+    using const by auto
+  moreover have "(\<Union>i. space (M i)) = space (M i)"
+    using const[THEN sets_eq_imp_space_eq] by auto
+  moreover have "\<And>i. sets (M i) \<subseteq> Pow (space (M i))"
+    by (auto dest: sets.sets_into_space)
+  ultimately show ?sp ?st
+    by (simp_all add: SUP_measure_def)
+qed
+
+lemma emeasure_SUP_measure:
+  assumes const: "\<And>i j. sets (M i) = sets (M j)"
+    and mono: "mono (\<lambda>i. emeasure (M i))"
+  shows "emeasure (SUP_measure M) A = (SUP i. emeasure (M i) A)"
+proof cases
+  assume "A \<in> sets (SUP_measure M)"
+  show ?thesis
+  proof (rule emeasure_measure_of[OF SUP_measure_def])
+    show "countably_additive (sets (SUP_measure M)) (\<lambda>A. SUP i. emeasure (M i) A)"
+    proof (rule countably_additiveI)
+      fix A :: "nat \<Rightarrow> 'a set" assume "range A \<subseteq> sets (SUP_measure M)"
+      then have "\<And>i j. A i \<in> sets (M j)"
+        using sets_SUP_measure[of M, OF const] by simp
+      moreover assume "disjoint_family A"
+      ultimately show "(\<Sum>i. SUP ia. emeasure (M ia) (A i)) = (SUP i. emeasure (M i) (\<Union>i. A i))"
+        using mono by (subst suminf_SUP_eq) (auto simp: mono_def le_fun_def intro!: SUP_cong suminf_emeasure)
+    qed
+    show "positive (sets (SUP_measure M)) (\<lambda>A. SUP i. emeasure (M i) A)"
+      by (auto simp: positive_def intro: SUP_upper2)
+    show "(\<Union>i. sets (M i)) \<subseteq> Pow (\<Union>i. space (M i))"
+      using sets.sets_into_space by auto
+  qed fact
+next
+  assume "A \<notin> sets (SUP_measure M)"
+  with sets_SUP_measure[of M, OF const] show ?thesis
+    by (simp add: emeasure_notin_sets)
+qed
+
+end
diff -r 7338eb25226c -r c38d8f139bbc src/HOL/Probability/Measure_Space.thy
--- a/src/HOL/Probability/Measure_Space.thy	Tue Oct 07 20:59:46 2014 +0200
+++ b/src/HOL/Probability/Measure_Space.thy	Tue Oct 07 21:01:31 2014 +0200
@@ -1643,6 +1643,10 @@
   "X \<subseteq> A \<Longrightarrow> infinite X \<Longrightarrow> emeasure (count_space A) X = \<infinity>"
   using emeasure_count_space[of X A] by simp
 
+lemma measure_count_space: "measure (count_space A) X = (if X \<subseteq> A then card X else 0)"
+  unfolding measure_def
+  by (cases "finite X") (simp_all add: emeasure_notin_sets)
+
 lemma emeasure_count_space_eq_0:
   "emeasure (count_space A) X = 0 \<longleftrightarrow> (X \<subseteq> A \<longrightarrow> X = {})"
 proof cases
@@ -1655,6 +1659,9 @@
   qed simp
 qed (simp add: emeasure_notin_sets)
 
+lemma space_empty: "space M = {} \<Longrightarrow> M = count_space {}"
+  by (rule measure_eqI) (simp_all add: space_empty_iff)
+
 lemma null_sets_count_space: "null_sets (count_space A) = { {} }"
   unfolding null_sets_def by (auto simp add: emeasure_count_space_eq_0)
 
diff -r 7338eb25226c -r c38d8f139bbc src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Tue Oct 07 20:59:46 2014 +0200
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Tue Oct 07 21:01:31 2014 +0200
@@ -748,6 +748,9 @@
 lemma nn_integral_nonneg: "0 \<le> integral\<^sup>N M f"
   by (auto intro!: SUP_upper2[of "\<lambda>x. 0"] simp: nn_integral_def le_fun_def)
 
+lemma nn_integral_le_0[simp]: "integral\<^sup>N M f \<le> 0 \<longleftrightarrow> integral\<^sup>N M f = 0"
+  using nn_integral_nonneg[of M f] by auto
+
 lemma nn_integral_not_MInfty[simp]: "integral\<^sup>N M f \<noteq> -\<infinity>"
   using nn_integral_nonneg[of M f] by auto
 
@@ -2187,6 +2190,10 @@
   using emeasure_uniform_measure[OF emeasure_neq_0_sets[OF A(1)] B] A
   by (cases "emeasure M A" "emeasure M (A \<inter> B)" rule: ereal2_cases) (simp_all add: measure_def)
 
+lemma AE_uniform_measureI:
+  "A \<in> sets M \<Longrightarrow> (AE x in M. x \<in> A \<longrightarrow> P x) \<Longrightarrow> (AE x in uniform_measure M A. P x)"
+  unfolding uniform_measure_def by (auto simp: AE_density)
+
 subsubsection {* Uniform count measure *}
 
 definition "uniform_count_measure A = point_measure A (\<lambda>x. 1 / card A)"
diff -r 7338eb25226c -r c38d8f139bbc src/HOL/Probability/Probability.thy
--- a/src/HOL/Probability/Probability.thy	Tue Oct 07 20:59:46 2014 +0200
+++ b/src/HOL/Probability/Probability.thy	Tue Oct 07 21:01:31 2014 +0200
@@ -7,6 +7,7 @@
   Distributions
   Probability_Mass_Function
   Stream_Space
+  Giry_Monad
 begin
 
 end
diff -r 7338eb25226c -r c38d8f139bbc src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Oct 07 20:59:46 2014 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Oct 07 21:01:31 2014 +0200
@@ -1,20 +1,10 @@
+(*  Title:      HOL/Probability/Probability_Mass_Function.thy
+    Author:     Johannes Hölzl, TU München *)
+
 theory Probability_Mass_Function
   imports Probability_Measure
 begin
 
-lemma sets_Pair: "{x} \<in> sets M1 \<Longrightarrow> {y} \<in> sets M2 \<Longrightarrow> {(x, y)} \<in> sets (M1 \<Otimes>\<^sub>M M2)"
-  using pair_measureI[of "{x}" M1 "{y}" M2] by simp
-
-lemma finite_subset_card:
-  assumes X: "infinite X" shows "\<exists>A\<subseteq>X. finite A \<and> card A = n"
-proof (induct n)
-  case (Suc n) then guess A .. note A = this
-  with X obtain x where "x \<in> X" "x \<notin> A"
-    by (metis subset_antisym subset_eq)
-  with A show ?case  
-    by (intro exI[of _ "insert x A"]) auto
-qed (simp cong: conj_cong)
-
 lemma (in prob_space) countable_support:
   "countable {x. measure M {x} \<noteq> 0}"
 proof -
@@ -25,7 +15,7 @@
   proof (rule ccontr)
     fix n assume "infinite {x. inverse (Suc n) < ?m x}" (is "infinite ?X")
     then obtain X where "finite X" "card X = Suc (Suc n)" "X \<subseteq> ?X"
-      by (metis finite_subset_card)
+      by (metis infinite_arbitrarily_large)
     from this(3) have *: "\<And>x. x \<in> X \<Longrightarrow> 1 / Suc n \<le> ?m x" 
       by (auto simp: inverse_eq_divide)
     { fix x assume "x \<in> X"
@@ -46,17 +36,10 @@
     unfolding * by (intro countable_UN countableI_type countable_finite[OF **])
 qed
 
-lemma measure_count_space: "measure (count_space A) X = (if X \<subseteq> A then card X else 0)"
-  unfolding measure_def
-  by (cases "finite X") (simp_all add: emeasure_notin_sets)
-
 typedef 'a pmf = "{M :: 'a measure. prob_space M \<and> sets M = UNIV \<and> (AE x in M. measure M {x} \<noteq> 0)}"
   morphisms measure_pmf Abs_pmf
-  apply (intro exI[of _ "uniform_measure (count_space UNIV) {undefined}"])
-  apply (auto intro!: prob_space_uniform_measure simp: measure_count_space)
-  apply (subst uniform_measure_def)
-  apply (simp add: AE_density AE_count_space split: split_indicator)
-  done
+  by (intro exI[of _ "uniform_measure (count_space UNIV) {undefined}"])
+     (auto intro!: prob_space_uniform_measure AE_uniform_measureI)
 
 declare [[coercion measure_pmf]]
 
diff -r 7338eb25226c -r c38d8f139bbc src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Tue Oct 07 20:59:46 2014 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Tue Oct 07 21:01:31 2014 +0200
@@ -1759,6 +1759,10 @@
 lemma in_measure_of[intro, simp]: "M \<subseteq> Pow \<Omega> \<Longrightarrow> A \<in> M \<Longrightarrow> A \<in> sets (measure_of \<Omega> M \<mu>)"
   by auto
 
+lemma space_empty_iff: "space N = {} \<longleftrightarrow> sets N = {{}}"
+  by (metis Pow_empty Sup_bot_conv(1) cSup_singleton empty_iff
+            sets.sigma_sets_eq sets.space_closed sigma_sets_top subset_singletonD)
+
 subsubsection {* Constructing simple @{typ "'a measure"} *}
 
 lemma emeasure_measure_of:
@@ -2154,6 +2158,10 @@
     unfolding measurable_def by auto
 qed
 
+lemma measurable_empty_iff: 
+  "space N = {} \<Longrightarrow> f \<in> measurable M N \<longleftrightarrow> space M = {}"
+  by (auto simp add: measurable_def Pi_iff)
+
 subsubsection {* Extend measure *}
 
 definition "extend_measure \<Omega> I G \<mu> =
@@ -2214,7 +2222,7 @@
   using emeasure_extend_measure[OF M _ _ ms(2,3), of "(i,j)"] eq ms(1) `I i j`
   by (auto simp: subset_eq)
 
-subsubsection {* Supremum of a set of \sigma-algebras *}
+subsubsection {* Supremum of a set of $\sigma$-algebras *}
 
 definition "Sup_sigma M = sigma (\<Union>x\<in>M. space x) (\<Union>x\<in>M. sets x)"
 
@@ -2266,7 +2274,7 @@
     using measurable_space[OF f] M by auto
 qed (auto intro: measurable_sets f dest: sets.sets_into_space)
 
-subsection {* The smallest \sigma-algebra regarding a function *}
+subsection {* The smallest $\sigma$-algebra regarding a function *}
 
 definition
   "vimage_algebra X f M = sigma X {f -` A \<inter> X | A. A \<in> sets M}"
diff -r 7338eb25226c -r c38d8f139bbc src/HOL/Probability/Stream_Space.thy
--- a/src/HOL/Probability/Stream_Space.thy	Tue Oct 07 20:59:46 2014 +0200
+++ b/src/HOL/Probability/Stream_Space.thy	Tue Oct 07 21:01:31 2014 +0200
@@ -1,7 +1,10 @@
+(*  Title:      HOL/Probability/Stream_Space.thy
+    Author:     Johannes Hölzl, TU München *)
+
 theory Stream_Space
 imports
   Infinite_Product_Measure
-  "~~/src/HOL/Datatype_Examples/Stream"
+  "~~/src/HOL/Library/Stream"
 begin
 
 lemma stream_eq_Stream_iff: "s = x ## t \<longleftrightarrow> (shd s = x \<and> stl s = t)"
@@ -10,15 +13,6 @@
 lemma Stream_snth: "(x ## s) !! n = (case n of 0 \<Rightarrow> x | Suc n \<Rightarrow> s !! n)"
   by (cases n) simp_all
 
-lemma sets_PiM_cong: assumes "I = J" "\<And>i. i \<in> J \<Longrightarrow> sets (M i) = sets (N i)" shows "sets (PiM I M) = sets (PiM J N)"
-  using assms sets_eq_imp_space_eq[OF assms(2)] by (simp add: sets_PiM_single cong: PiE_cong conj_cong)
-
-lemma nn_integral_le_0[simp]: "integral\<^sup>N M f \<le> 0 \<longleftrightarrow> integral\<^sup>N M f = 0"
-  using nn_integral_nonneg[of M f] by auto
-
-lemma restrict_UNIV: "restrict f UNIV = f"
-  by (simp add: restrict_def)
-
 definition to_stream :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a stream" where
   "to_stream X = smap X nats"
 
diff -r 7338eb25226c -r c38d8f139bbc src/HOL/Probability/document/root.tex
--- a/src/HOL/Probability/document/root.tex	Tue Oct 07 20:59:46 2014 +0200
+++ b/src/HOL/Probability/document/root.tex	Tue Oct 07 21:01:31 2014 +0200
@@ -6,6 +6,7 @@
 \usepackage[only,bigsqcap]{stmaryrd}
 \usepackage[utf8]{inputenc}
 \usepackage{pdfsetup}
+\usepackage[english]{babel}
 
 \urlstyle{rm}
 \isabellestyle{it}