HOL-Probability: move stopping time from AFP/Markov_Models

--- a/src/HOL/Analysis/Borel_Space.thy	Thu Oct 20 18:41:58 2016 +0200
+++ b/src/HOL/Analysis/Borel_Space.thy	Thu Oct 20 18:41:59 2016 +0200
@@ -345,6 +345,14 @@
   "A \<in> sets borel \<Longrightarrow> insert x A \<in> sets (borel :: 'a::t1_space measure)"
   unfolding insert_def by (rule sets.Un) auto
 
+lemma sets_borel_eq_count_space: "sets (borel :: 'a::{countable, t2_space} measure) = count_space UNIV"
+proof -
+  have "(\<Union>a\<in>A. {a}) \<in> sets borel" for A :: "'a set"
+    by (intro sets.countable_UN') auto
+  then show ?thesis
+    by auto
+qed
+
 lemma borel_comp[measurable]: "A \<in> sets borel \<Longrightarrow> - A \<in> sets borel"
   unfolding Compl_eq_Diff_UNIV by simp
 

--- a/src/HOL/Analysis/Extended_Real_Limits.thy	Thu Oct 20 18:41:58 2016 +0200
+++ b/src/HOL/Analysis/Extended_Real_Limits.thy	Thu Oct 20 18:41:59 2016 +0200
@@ -56,6 +56,15 @@
     by simp
 qed
 
+instance enat :: second_countable_topology
+proof
+  show "\<exists>B::enat set set. countable B \<and> open = generate_topology B"
+  proof (intro exI conjI)
+    show "countable (range lessThan \<union> range greaterThan::enat set set)"
+      by auto
+  qed (simp add: open_enat_def)
+qed
+
 instance ereal :: second_countable_topology
 proof (standard, intro exI conjI)
   let ?B = "(\<Union>r\<in>\<rat>. {{..< r}, {r <..}} :: ereal set set)"

--- a/src/HOL/Analysis/Measurable.thy	Thu Oct 20 18:41:58 2016 +0200
+++ b/src/HOL/Analysis/Measurable.thy	Thu Oct 20 18:41:59 2016 +0200
@@ -646,6 +646,14 @@
   shows "liminf A \<in> sets M"
 by (subst liminf_SUP_INF, auto)
 
+lemma measurable_case_enat[measurable (raw)]:
+  assumes f: "f \<in> M \<rightarrow>\<^sub>M count_space UNIV" and g: "\<And>i. g i \<in> M \<rightarrow>\<^sub>M N" and h: "h \<in> M \<rightarrow>\<^sub>M N"
+  shows "(\<lambda>x. case f x of enat i \<Rightarrow> g i x | \<infinity> \<Rightarrow> h x) \<in> M \<rightarrow>\<^sub>M N"
+  apply (rule measurable_compose_countable[OF _ f])
+  subgoal for i
+    by (cases i) (auto intro: g h)
+  done
+
 hide_const (open) pred
 
 end

--- a/src/HOL/Analysis/Measure_Space.thy	Thu Oct 20 18:41:58 2016 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy	Thu Oct 20 18:41:59 2016 +0200
@@ -1469,6 +1469,9 @@
 lemma distr_id[simp]: "distr N N (\<lambda>x. x) = N"
   by (rule measure_eqI) (auto simp: emeasure_distr)
 
+lemma distr_id2: "sets M = sets N \<Longrightarrow> distr N M (\<lambda>x. x) = N"
+  by (rule measure_eqI) (auto simp: emeasure_distr)
+
 lemma measure_distr:
   "f \<in> measurable M N \<Longrightarrow> S \<in> sets N \<Longrightarrow> measure (distr M N f) S = measure M (f -` S \<inter> space M)"
   by (simp add: emeasure_distr measure_def)
@@ -3516,6 +3519,11 @@
   finally show ?thesis .
 qed
 
+lemma measurable_SUP2:
+  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f \<in> measurable N (M i)) \<Longrightarrow>
+    (\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> space (M i) = space (M j)) \<Longrightarrow> f \<in> measurable N (SUP i:I. M i)"
+  by (auto intro!: measurable_Sup2)
+
 lemma sets_Sup_sigma:
   assumes [simp]: "M \<noteq> {}" and M: "\<And>m. m \<in> M \<Longrightarrow> m \<subseteq> Pow \<Omega>"
   shows "sets (SUP m:M. sigma \<Omega> m) = sets (sigma \<Omega> (\<Union>M))"

--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Oct 20 18:41:58 2016 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Oct 20 18:41:59 2016 +0200
@@ -458,6 +458,11 @@
        (fastforce simp: topological_space_class.topological_basis_def)+
 qed
 
+instance nat :: second_countable_topology
+proof
+  show "\<exists>B::nat set set. countable B \<and> open = generate_topology B"
+    by (intro exI[of _ "range lessThan \<union> range greaterThan"]) (auto simp: open_nat_def)
+qed
 
 lemma countable_separating_set_linorder1:
   shows "\<exists>B::('a::{linorder_topology, second_countable_topology} set). countable B \<and> (\<forall>x y. x < y \<longrightarrow> (\<exists>b \<in> B. x < b \<and> b \<le> y))"

--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Thu Oct 20 18:41:58 2016 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Thu Oct 20 18:41:59 2016 +0200
@@ -1131,6 +1131,9 @@
 lemma enn2real_positive_iff: "0 < enn2real x \<longleftrightarrow> (0 < x \<and> x < top)"
   by (cases x rule: ennreal_cases) auto
 
+lemma enn2real_eq_1_iff[simp]: "enn2real x = 1 \<longleftrightarrow> x = 1"
+  by (cases x) auto
+
 subsection \<open>Coercion from @{typ enat} to @{typ ennreal}\<close>
 
 

--- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Thu Oct 20 18:41:58 2016 +0200
+++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Thu Oct 20 18:41:59 2016 +0200
@@ -662,7 +662,7 @@
 lemma sfilter_not_P[simp]: "\<not> P (shd s) \<Longrightarrow> sfilter P s = sfilter P (stl s)"
   using sfilter_Stream[of P "shd s" "stl s"] by simp
 
-lemma sfilter_eq: 
+lemma sfilter_eq:
   assumes "ev (holds P) s"
   shows "sfilter P s = x ## s' \<longleftrightarrow>
     P x \<and> (not (holds P) suntil (HLD {x} aand nxt (\<lambda>s. sfilter P s = s'))) s"
@@ -685,7 +685,7 @@
 proof
   assume "alw Q (sfilter P s)" with * show "alw (\<lambda>x. Q (sfilter P x)) s"
   proof (coinduction arbitrary: s rule: alw_coinduct)
-    case (stl s) 
+    case (stl s)
     then have "ev (holds P) s"
       by blast
     from this stl show ?case
@@ -694,7 +694,7 @@
 next
   assume "alw (\<lambda>x. Q (sfilter P x)) s" with * show "alw Q (sfilter P s)"
   proof (coinduction arbitrary: s rule: alw_coinduct)
-    case (stl s) 
+    case (stl s)
     then have "ev (holds P) s"
       by blast
     from this stl show ?case
@@ -767,4 +767,22 @@
 lemma hld_smap': "HLD x (smap f s) = HLD (f -` x) s"
   by (simp add: HLD_def)
 
+lemma pigeonhole_stream:
+  assumes "alw (HLD s) \<omega>"
+  assumes "finite s"
+  shows "\<exists>x\<in>s. alw (ev (HLD {x})) \<omega>"
+proof -
+  have "\<forall>i\<in>UNIV. \<exists>x\<in>s. \<omega> !! i = x"
+    using `alw (HLD s) \<omega>` by (simp add: alw_iff_sdrop HLD_iff)
+  from pigeonhole_infinite_rel[OF infinite_UNIV_nat `finite s` this]
+  show ?thesis
+    by (simp add: HLD_iff infinite_iff_alw_ev[symmetric])
+qed
+
+lemma ev_eq_suntil: "ev P \<omega> \<longleftrightarrow> (not P suntil P) \<omega>"
+proof
+  assume "ev P \<omega>" then show "((\<lambda>xs. \<not> P xs) suntil P) \<omega>"
+    by (induction rule: ev_induct_strong) (auto intro: suntil.intros)
+qed (auto simp: ev_suntil)
+
 end

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

--- a/src/HOL/Probability/Giry_Monad.thy	Thu Oct 20 18:41:58 2016 +0200
+++ b/src/HOL/Probability/Giry_Monad.thy	Thu Oct 20 18:41:59 2016 +0200
@@ -1778,4 +1778,10 @@
   shows "space (M \<bind> f) = space B"
   using M by (intro space_bind[OF sets_kernel[OF f]]) auto
 
+lemma bind_distr_return:
+  "f \<in> M \<rightarrow>\<^sub>M N \<Longrightarrow> g \<in> N \<rightarrow>\<^sub>M L \<Longrightarrow> space M \<noteq> {} \<Longrightarrow>
+    distr M N f \<bind> (\<lambda>x. return L (g x)) = distr M L (\<lambda>x. g (f x))"
+  by (subst bind_distr[OF _ measurable_compose[OF _ return_measurable]])
+     (auto intro!: bind_return_distr')
+
 end

--- a/src/HOL/Probability/Probability.thy	Thu Oct 20 18:41:58 2016 +0200
+++ b/src/HOL/Probability/Probability.thy	Thu Oct 20 18:41:59 2016 +0200
@@ -13,6 +13,7 @@
   Stream_Space
   Conditional_Expectation
   Essential_Supremum
+  Stopping_Time
 begin
 
 end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Stopping_Time.thy	Thu Oct 20 18:41:59 2016 +0200
@@ -0,0 +1,262 @@
+(* Author: Johannes Hölzl <[e-mail]> *)
+
+section {* Stopping times *}
+
+theory Stopping_Time
+  imports "../Analysis/Analysis"
+begin
+
+subsection \<open>Stopping Time\<close>
+
+text \<open>This is also called strong stopping time. Then stopping time is T with alternative is
+  \<open>T x < t\<close> measurable.\<close>
+
+definition stopping_time :: "('t::linorder \<Rightarrow> 'a measure) \<Rightarrow> ('a \<Rightarrow> 't) \<Rightarrow> bool"
+where
+  "stopping_time F T = (\<forall>t. Measurable.pred (F t) (\<lambda>x. T x \<le> t))"
+
+lemma stopping_time_cong: "(\<And>t x. x \<in> space (F t) \<Longrightarrow> T x = S x) \<Longrightarrow> stopping_time F T = stopping_time F S"
+  unfolding stopping_time_def by (intro arg_cong[where f=All] ext measurable_cong) simp
+
+lemma stopping_timeD: "stopping_time F T \<Longrightarrow> Measurable.pred (F t) (\<lambda>x. T x \<le> t)"
+  by (auto simp: stopping_time_def)
+
+lemma stopping_timeD2: "stopping_time F T \<Longrightarrow> Measurable.pred (F t) (\<lambda>x. t < T x)"
+  unfolding not_le[symmetric] by (auto intro: stopping_timeD Measurable.pred_intros_logic)
+
+lemma stopping_timeI[intro?]: "(\<And>t. Measurable.pred (F t) (\<lambda>x. T x \<le> t)) \<Longrightarrow> stopping_time F T"
+  by (auto simp: stopping_time_def)
+
+lemma measurable_stopping_time:
+  fixes T :: "'a \<Rightarrow> 't::{linorder_topology, second_countable_topology}"
+  assumes T: "stopping_time F T"
+    and M: "\<And>t. sets (F t) \<subseteq> sets M" "\<And>t. space (F t) = space M"
+  shows "T \<in> M \<rightarrow>\<^sub>M borel"
+proof (rule borel_measurableI_le)
+  show "{x \<in> space M. T x \<le> t} \<in> sets M" for t
+    using stopping_timeD[OF T] M by (auto simp: Measurable.pred_def)
+qed
+
+lemma stopping_time_const: "stopping_time F (\<lambda>x. c)"
+  by (auto simp: stopping_time_def)
+
+lemma stopping_time_min:
+  "stopping_time F T \<Longrightarrow> stopping_time F S \<Longrightarrow> stopping_time F (\<lambda>x. min (T x) (S x))"
+  by (auto simp: stopping_time_def min_le_iff_disj intro!: pred_intros_logic)
+
+lemma stopping_time_max:
+  "stopping_time F T \<Longrightarrow> stopping_time F S \<Longrightarrow> stopping_time F (\<lambda>x. max (T x) (S x))"
+  by (auto simp: stopping_time_def intro!: pred_intros_logic)
+
+section \<open>Filtration\<close>
+
+locale filtration =
+  fixes \<Omega> :: "'a set" and F :: "'t::{linorder_topology, second_countable_topology} \<Rightarrow> 'a measure"
+  assumes space_F: "\<And>i. space (F i) = \<Omega>"
+  assumes sets_F_mono: "\<And>i j. i \<le> j \<Longrightarrow> sets (F i) \<le> sets (F j)"
+begin
+
+subsection \<open>$\sigma$-algebra of a Stopping Time\<close>
+
+definition pre_sigma :: "('a \<Rightarrow> 't) \<Rightarrow> 'a measure"
+where
+  "pre_sigma T = sigma \<Omega> {A. \<forall>t. {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)}"
+
+lemma space_pre_sigma: "space (pre_sigma T) = \<Omega>"
+  unfolding pre_sigma_def using sets.space_closed[of "F _"]
+  by (intro space_measure_of) (auto simp: space_F)
+
+lemma measure_pre_sigma[simp]: "emeasure (pre_sigma T) = (\<lambda>_. 0)"
+  by (simp add: pre_sigma_def emeasure_sigma)
+
+lemma sigma_algebra_pre_sigma:
+  assumes T: "stopping_time F T"
+  shows "sigma_algebra \<Omega> {A. \<forall>t. {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)}"
+  unfolding sigma_algebra_iff2
+proof (intro sigma_algebra_iff2[THEN iffD2] conjI ballI allI impI CollectI)
+  show "{A. \<forall>t. {\<omega> \<in> A. T \<omega> \<le> t} \<in> sets (F t)} \<subseteq> Pow \<Omega>"
+    using sets.space_closed[of "F _"] by (auto simp: space_F)
+next
+  fix A t assume "A \<in> {A. \<forall>t. {\<omega> \<in> A. T \<omega> \<le> t} \<in> sets (F t)}"
+  then have "{\<omega> \<in> space (F t). T \<omega> \<le> t} - {\<omega> \<in> A. T \<omega> \<le> t} \<in> sets (F t)"
+    using T stopping_timeD[measurable] by auto
+  also have "{\<omega> \<in> space (F t). T \<omega> \<le> t} - {\<omega> \<in> A. T \<omega> \<le> t} = {\<omega> \<in> \<Omega> - A. T \<omega> \<le> t}"
+    by (auto simp: space_F)
+  finally show "{\<omega> \<in> \<Omega> - A. T \<omega> \<le> t} \<in> sets (F t)" .
+next
+  fix AA :: "nat \<Rightarrow> 'a set" and t assume "range AA \<subseteq> {A. \<forall>t. {\<omega> \<in> A. T \<omega> \<le> t} \<in> sets (F t)}"
+  then have "(\<Union>i. {\<omega> \<in> AA i. T \<omega> \<le> t}) \<in> sets (F t)" for t
+    by auto
+  also have "(\<Union>i. {\<omega> \<in> AA i. T \<omega> \<le> t}) = {\<omega> \<in> UNION UNIV AA. T \<omega> \<le> t}"
+    by auto
+  finally show "{\<omega> \<in> UNION UNIV AA. T \<omega> \<le> t} \<in> sets (F t)" .
+qed auto
+
+lemma sets_pre_sigma: "stopping_time F T \<Longrightarrow> sets (pre_sigma T) = {A. \<forall>t. {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)}"
+  unfolding pre_sigma_def by (rule sigma_algebra.sets_measure_of_eq[OF sigma_algebra_pre_sigma])
+
+lemma sets_pre_sigmaI: "stopping_time F T \<Longrightarrow> (\<And>t. {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)) \<Longrightarrow> A \<in> sets (pre_sigma T)"
+  unfolding sets_pre_sigma by auto
+
+lemma pred_pre_sigmaI:
+  assumes T: "stopping_time F T"
+  shows "(\<And>t. Measurable.pred (F t) (\<lambda>\<omega>. P \<omega> \<and> T \<omega> \<le> t)) \<Longrightarrow> Measurable.pred (pre_sigma T) P"
+  unfolding pred_def space_F space_pre_sigma by (intro sets_pre_sigmaI[OF T]) simp
+
+lemma sets_pre_sigmaD: "stopping_time F T \<Longrightarrow> A \<in> sets (pre_sigma T) \<Longrightarrow> {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)"
+  unfolding sets_pre_sigma by auto
+
+lemma stopping_time_le_const: "stopping_time F T \<Longrightarrow> s \<le> t \<Longrightarrow> Measurable.pred (F t) (\<lambda>\<omega>. T \<omega> \<le> s)"
+  using stopping_timeD[of F T] sets_F_mono[of _ t] by (auto simp: pred_def space_F)
+
+lemma measurable_stopping_time_pre_sigma:
+  assumes T: "stopping_time F T" shows "T \<in> pre_sigma T \<rightarrow>\<^sub>M borel"
+proof (intro borel_measurableI_le sets_pre_sigmaI[OF T])
+  fix t t'
+  have "{\<omega>\<in>space (F (min t' t)). T \<omega> \<le> min t' t} \<in> sets (F (min t' t))"
+    using T unfolding pred_def[symmetric] by (rule stopping_timeD)
+  also have "\<dots> \<subseteq> sets (F t)"
+    by (rule sets_F_mono) simp
+  finally show "{\<omega> \<in> {x \<in> space (pre_sigma T). T x \<le> t'}. T \<omega> \<le> t} \<in> sets (F t)"
+    by (simp add: space_pre_sigma space_F)
+qed
+
+lemma mono_pre_sigma:
+  assumes T: "stopping_time F T" and S: "stopping_time F S"
+    and le: "\<And>\<omega>. \<omega> \<in> \<Omega> \<Longrightarrow> T \<omega> \<le> S \<omega>"
+  shows "sets (pre_sigma T) \<subseteq> sets (pre_sigma S)"
+  unfolding sets_pre_sigma[OF S] sets_pre_sigma[OF T]
+proof safe
+  interpret sigma_algebra \<Omega> "{A. \<forall>t. {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)}"
+    using T by (rule sigma_algebra_pre_sigma)
+  fix A t assume A: "\<forall>t. {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)"
+  then have "A \<subseteq> \<Omega>"
+    using sets_into_space by auto
+  from A have "{\<omega>\<in>A. T \<omega> \<le> t} \<inter> {\<omega>\<in>space (F t). S \<omega> \<le> t} \<in> sets (F t)"
+    using stopping_timeD[OF S] by (auto simp: pred_def)
+  also have "{\<omega>\<in>A. T \<omega> \<le> t} \<inter> {\<omega>\<in>space (F t). S \<omega> \<le> t} = {\<omega>\<in>A. S \<omega> \<le> t}"
+    using \<open>A \<subseteq> \<Omega>\<close> sets_into_space[of A] le by (auto simp: space_F intro: order_trans)
+  finally show "{\<omega>\<in>A. S \<omega> \<le> t} \<in> sets (F t)"
+    by auto
+qed
+
+lemma stopping_time_less_const:
+  assumes T: "stopping_time F T" shows "Measurable.pred (F t) (\<lambda>\<omega>. T \<omega> < t)"
+proof -
+  guess D :: "'t set" by (rule countable_dense_setE)
+  note D = this
+  show ?thesis
+  proof cases
+    assume *: "\<forall>t'<t. \<exists>t''. t' < t'' \<and> t'' < t"
+    { fix t' assume "t' < t"
+      with * have "{t' <..< t} \<noteq> {}"
+        by fastforce
+      with D(2)[OF _ this]
+      have "\<exists>d\<in>D. t'< d \<and> d < t"
+        by auto }
+    note ** = this
+
+    show ?thesis
+    proof (rule measurable_cong[THEN iffD2])
+      show "T \<omega> < t \<longleftrightarrow> (\<exists>r\<in>{r\<in>D. r < t}. T \<omega> \<le> r)" for \<omega>
+        by (auto dest: ** intro: less_imp_le)
+      show "Measurable.pred (F t) (\<lambda>w. \<exists>r\<in>{r \<in> D. r < t}. T w \<le> r)"
+        by (intro measurable_pred_countable stopping_time_le_const[OF T] countable_Collect D) auto
+    qed
+  next
+    assume "\<not> (\<forall>t'<t. \<exists>t''. t' < t'' \<and> t'' < t)"
+    then obtain t' where t': "t' < t" "\<And>t''. t'' < t \<Longrightarrow> t'' \<le> t'"
+      by (auto simp: not_less[symmetric])
+    show ?thesis
+    proof (rule measurable_cong[THEN iffD2])
+      show "T \<omega> < t \<longleftrightarrow> T \<omega> \<le> t'" for \<omega>
+        using t' by auto
+      show "Measurable.pred (F t) (\<lambda>w. T w \<le> t')"
+        using \<open>t'<t\<close> by (intro stopping_time_le_const[OF T]) auto
+    qed
+  qed
+qed
+
+lemma stopping_time_eq_const: "stopping_time F T \<Longrightarrow> Measurable.pred (F t) (\<lambda>\<omega>. T \<omega> = t)"
+  unfolding eq_iff using stopping_time_less_const[of T t]
+  by (intro pred_intros_logic stopping_time_le_const) (auto simp: not_less[symmetric] )
+
+lemma stopping_time_less:
+  assumes T: "stopping_time F T" and S: "stopping_time F S"
+  shows "Measurable.pred (pre_sigma T) (\<lambda>\<omega>. T \<omega> < S \<omega>)"
+proof (rule pred_pre_sigmaI[OF T])
+  fix t
+  obtain D :: "'t set"
+    where [simp]: "countable D" and semidense_D: "\<And>x y. x < y \<Longrightarrow> (\<exists>b\<in>D. x \<le> b \<and> b < y)"
+    using countable_separating_set_linorder2 by auto
+  show "Measurable.pred (F t) (\<lambda>\<omega>. T \<omega> < S \<omega> \<and> T \<omega> \<le> t)"
+  proof (rule measurable_cong[THEN iffD2])
+    let ?f = "\<lambda>\<omega>. if T \<omega> = t then \<not> S \<omega> \<le> t else \<exists>s\<in>{s\<in>D. s \<le> t}. T \<omega> \<le> s \<and> \<not> (S \<omega> \<le> s)"
+    { fix \<omega> assume "T \<omega> \<le> t" "T \<omega> \<noteq> t" "T \<omega> < S \<omega>"
+      then have "T \<omega> < min t (S \<omega>)"
+        by auto
+      then obtain r where "r \<in> D" "T \<omega> \<le> r" "r < min t (S \<omega>)"
+        by (metis semidense_D)
+      then have "\<exists>s\<in>{s\<in>D. s \<le> t}. T \<omega> \<le> s \<and> s < S \<omega>"
+        by auto }
+    then show "(T \<omega> < S \<omega> \<and> T \<omega> \<le> t) = ?f \<omega>" for \<omega>
+      by (auto simp: not_le)
+    show "Measurable.pred (F t) ?f"
+      by (intro pred_intros_logic measurable_If measurable_pred_countable countable_Collect
+                stopping_time_le_const predE stopping_time_eq_const T S)
+         auto
+  qed
+qed
+
+end
+
+lemma stopping_time_SUP_enat:
+  fixes T :: "nat \<Rightarrow> ('a \<Rightarrow> enat)"
+  shows "(\<And>i. stopping_time F (T i)) \<Longrightarrow> stopping_time F (SUP i. T i)"
+  unfolding stopping_time_def SUP_apply SUP_le_iff by (auto intro!: pred_intros_countable)
+
+lemma less_eSuc_iff: "a < eSuc b \<longleftrightarrow> (a \<le> b \<and> a \<noteq> \<infinity>)"
+  by (cases a) auto
+
+lemma stopping_time_Inf_enat:
+  fixes F :: "enat \<Rightarrow> 'a measure"
+  assumes F: "filtration \<Omega> F"
+  assumes P: "\<And>i. Measurable.pred (F i) (P i)"
+  shows "stopping_time F (\<lambda>\<omega>. Inf {i. P i \<omega>})"
+proof (rule stopping_timeI, cases)
+  fix t :: enat assume "t = \<infinity>" then show "Measurable.pred (F t) (\<lambda>\<omega>. Inf {i. P i \<omega>} \<le> t)"
+    by auto
+next
+  fix t :: enat assume "t \<noteq> \<infinity>"
+  moreover
+  { fix i \<omega> assume "Inf {i. P i \<omega>} \<le> t"
+    with \<open>t \<noteq> \<infinity>\<close> have "(\<exists>i\<le>t. P i \<omega>)"
+      unfolding Inf_le_iff by (cases t) (auto elim!: allE[of _ "eSuc t"] simp: less_eSuc_iff) }
+  ultimately have *: "\<And>\<omega>. Inf {i. P i \<omega>} \<le> t \<longleftrightarrow> (\<exists>i\<in>{..t}. P i \<omega>)"
+    by (auto intro!: Inf_lower2)
+  show "Measurable.pred (F t) (\<lambda>\<omega>. Inf {i. P i \<omega>} \<le> t)"
+    unfolding * using filtration.sets_F_mono[OF F, of _ t] P
+    by (intro pred_intros_countable_bounded) (auto simp: pred_def filtration.space_F[OF F])
+qed
+
+lemma stopping_time_Inf_nat:
+  fixes F :: "nat \<Rightarrow> 'a measure"
+  assumes F: "filtration \<Omega> F"
+  assumes P: "\<And>i. Measurable.pred (F i) (P i)" and wf: "\<And>i \<omega>. \<omega> \<in> \<Omega> \<Longrightarrow> \<exists>n. P n \<omega>"
+  shows "stopping_time F (\<lambda>\<omega>. Inf {i. P i \<omega>})"
+  unfolding stopping_time_def
+proof (intro allI, subst measurable_cong)
+  fix t \<omega> assume "\<omega> \<in> space (F t)"
+  then have "\<omega> \<in> \<Omega>"
+    using filtration.space_F[OF F] by auto
+  from wf[OF this] have "((LEAST n. P n \<omega>) \<le> t) = (\<exists>i\<le>t. P i \<omega>)"
+    by (rule LeastI2_wellorder_ex) auto
+  then show "(Inf {i. P i \<omega>} \<le> t) = (\<exists>i\<in>{..t}. P i \<omega>)"
+    by (simp add: Inf_nat_def Bex_def)
+next
+  fix t from P show "Measurable.pred (F t) (\<lambda>w. \<exists>i\<in>{..t}. P i w)"
+    using filtration.sets_F_mono[OF F, of _ t]
+    by (intro pred_intros_countable_bounded) (auto simp: pred_def filtration.space_F[OF F])
+qed
+
+end

--- a/src/HOL/Probability/Stream_Space.thy	Thu Oct 20 18:41:58 2016 +0200
+++ b/src/HOL/Probability/Stream_Space.thy	Thu Oct 20 18:41:59 2016 +0200
@@ -446,6 +446,17 @@
     by (cases "xs = []") (auto simp: * space_stream_space del: in_listsD)
 qed (auto simp: * ae sets_M del: in_listsD intro!: streams_sets)
 
+lemma sets_sstart[measurable]: "sstart \<Omega> xs \<in> sets (stream_space (count_space UNIV))"
+proof (induction xs)
+  case (Cons x xs)
+  note this[measurable]
+  have "sstart \<Omega> (x # xs) = {\<omega>\<in>space (stream_space (count_space UNIV)). \<omega> \<in> sstart \<Omega> (x # xs)}"
+    by (auto simp: space_stream_space)
+  also have "\<dots> \<in> sets (stream_space (count_space UNIV))"
+    unfolding in_sstart by measurable
+  finally show ?case .
+qed (auto intro!: streams_sets)
+
 primrec scylinder :: "'a set \<Rightarrow> 'a set list \<Rightarrow> 'a stream set"
 where
   "scylinder S [] = streams S"