diff --git a/thys/Ergodic_Theory/ME_Library_Complement.thy b/thys/Ergodic_Theory/ME_Library_Complement.thy
--- a/thys/Ergodic_Theory/ME_Library_Complement.thy
+++ b/thys/Ergodic_Theory/ME_Library_Complement.thy
@@ -1,61 +1,58 @@
 (*
    File:     ME_Library_Complement.thy
    Author:   Manuel Eberl, TU München
 *)
 theory ME_Library_Complement
   imports "HOL-Analysis.Analysis"
 begin
 
 (* TODO: could be put in the distribution *)
 
 subsection \<open>The trivial measurable space\<close>
 
 text \<open>
   The trivial measurable space is the smallest possible \<open>\<sigma>\<close>-algebra, i.e. only the empty set
   and everything.
 \<close>
 definition trivial_measure :: "'a set \<Rightarrow> 'a measure" where
   "trivial_measure X = sigma X {{}, X}"
 
 lemma space_trivial_measure [simp]: "space (trivial_measure X) = X"
   by (simp add: trivial_measure_def)
 
 lemma sets_trivial_measure: "sets (trivial_measure X) = {{}, X}"
   by (simp add: trivial_measure_def sigma_algebra_trivial sigma_algebra.sigma_sets_eq)
 
 lemma measurable_trivial_measure:
   assumes "f \<in> space M \<rightarrow> X" and "f -` X \<inter> space M \<in> sets M"
   shows   "f \<in> M \<rightarrow>\<^sub>M trivial_measure X"
   using assms unfolding measurable_def by (auto simp: sets_trivial_measure)
 
 lemma measurable_trivial_measure_iff:
   "f \<in> M \<rightarrow>\<^sub>M trivial_measure X \<longleftrightarrow> f \<in> space M \<rightarrow> X \<and> f -` X \<inter> space M \<in> sets M"
   unfolding measurable_def by (auto simp: sets_trivial_measure)
 
 
 subsection \<open>Pullback algebras\<close>
 
 text \<open>
   The pullback algebra $f^{-1}(\Sigma)$ of a \<open>\<sigma>\<close>-algebra $(\Omega, \Sigma)$ is the smallest
   \<open>\<sigma>\<close>-algebra such that $f$ is $f^{-1}(\Sigma)--\Sigma$-measurable.
 \<close>
 definition (in sigma_algebra) pullback_algebra :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'b set set" where
   "pullback_algebra f \<Omega>' = sigma_sets \<Omega>' {f -` A \<inter> \<Omega>' |A. A \<in> M}"
 
 lemma pullback_algebra_minimal:
   assumes "f \<in> M \<rightarrow>\<^sub>M N"
   shows   "sets.pullback_algebra N f (space M) \<subseteq> sets M"
 proof
   fix X assume "X \<in> sets.pullback_algebra N f (space M)"
   thus "X \<in> sets M"
     unfolding sets.pullback_algebra_def
     by induction (use assms in \<open>auto simp: measurable_def\<close>)
 qed
 
-lemma (in sigma_algebra) sigma_algebra_pullback: "sigma_algebra \<Omega>' (pullback_algebra f \<Omega>')"
-  unfolding pullback_algebra_def by (rule sigma_algebra_sigma_sets) auto
-
 lemma (in sigma_algebra) in_pullback_algebra: "A \<in> M \<Longrightarrow> f -` A \<inter> \<Omega>' \<in> pullback_algebra f \<Omega>'"
   unfolding pullback_algebra_def by (rule sigma_sets.Basic) auto
 
 end
\ No newline at end of file
diff --git a/thys/Ergodic_Theory/Shift_Operator.thy b/thys/Ergodic_Theory/Shift_Operator.thy
--- a/thys/Ergodic_Theory/Shift_Operator.thy
+++ b/thys/Ergodic_Theory/Shift_Operator.thy
@@ -1,268 +1,261 @@
 (*
    File:     Shift_Operator.thy
    Author:   Manuel Eberl, TU München
 *)
 section \<open>The shift operator on an infinite product measure\<close>
 theory Shift_Operator
   imports Ergodicity ME_Library_Complement
 begin
 
 text \<open>
   Let \<open>P\<close> be an an infinite product of i.i.d. instances of the distribution \<open>M\<close>.
   Then the shift operator is the map
   \[T(x_0, x_1, x_2, \ldots) = T(x_1, x_2, \ldots)\ .\]
   In this section, we define this operator and show that it is ergodic using Kolmogorov's
   0--1 law.
 \<close>
 
 locale shift_operator_ergodic = prob_space +
   fixes T :: "(nat \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a)" and P :: "(nat \<Rightarrow> 'a) measure"
   defines "T \<equiv> (\<lambda>f. f \<circ> Suc)"
   defines "P \<equiv> PiM (UNIV :: nat set) (\<lambda>_. M)"
 begin
 
 sublocale P: product_prob_space "\<lambda>_. M" UNIV
   by unfold_locales
 
 sublocale P: prob_space P
   by (simp add: prob_space_PiM prob_space_axioms P_def)
 
 lemma measurable_T [measurable]: "T \<in> P \<rightarrow>\<^sub>M P"
   unfolding P_def T_def o_def
   by (rule measurable_abs_UNIV[OF measurable_compose[OF measurable_component_singleton]]) auto
 
 
 text \<open>
   The \<open>n\<close>-th tail algebra $\mathcal{T}_n$ is, in some sense, the algebra in which we forget all
   information about all $x_i$ with \<open>i < n\<close>. We simply change the product algebra of \<open>P\<close> by replacing
   the algebra for each \<open>i < n\<close> with the trivial algebra that contains only the empty set and the
   entire space.
 \<close>
 definition tail_algebra :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) measure"
   where "tail_algebra n = PiM UNIV (\<lambda>i. if i < n then trivial_measure (space M) else M)"
 
 lemma tail_algebra_0 [simp]: "tail_algebra 0 = P"
   by (simp add: tail_algebra_def P_def)
 
 lemma space_tail_algebra [simp]: "space (tail_algebra n) = PiE UNIV (\<lambda>_. space M)"
   by (simp add: tail_algebra_def space_PiM PiE_def Pi_def)
 
 lemma measurable_P_component [measurable]: "P.random_variable M (\<lambda>f. f i)"
   unfolding P_def by measurable
 
 lemma P_component [simp]: "distr P M (\<lambda>f. f i) = M"
   unfolding P_def by (subst P.PiM_component) auto
 
 lemma indep_vars: "P.indep_vars (\<lambda>_. M) (\<lambda>i f. f i) UNIV"
   by (subst P.indep_vars_iff_distr_eq_PiM)
      (simp_all add: restrict_def distr_id2 P.PiM_component P_def)
 
 
 text \<open>
   The shift operator takes us from $\mathcal{T}_n$ to $\mathcal{T}_{n+1}$ (it forgets the
   information about one more variable):
 \<close>
 lemma measurable_T_tail: "T \<in> tail_algebra (Suc n) \<rightarrow>\<^sub>M tail_algebra n"
   unfolding T_def tail_algebra_def o_def
   by (rule measurable_abs_UNIV[OF measurable_compose[OF measurable_component_singleton]]) simp_all
 
 lemma measurable_funpow_T: "T ^^ n \<in> tail_algebra (m + n) \<rightarrow>\<^sub>M tail_algebra m"
 proof (induction n)
   case (Suc n)
   have "(T ^^ n) \<circ> T \<in> tail_algebra (m + Suc n) \<rightarrow>\<^sub>M tail_algebra m"
     by (rule measurable_comp[OF _ Suc]) (simp_all add: measurable_T_tail)
   thus ?case by (simp add: o_def funpow_swap1)
 qed auto
 
 lemma measurable_funpow_T': "T ^^ n \<in> tail_algebra n \<rightarrow>\<^sub>M P"
   using measurable_funpow_T[of n 0] by simp
 
 
 text \<open>
   The shift operator is clearly measure-preserving:
 \<close>
 lemma measure_preserving: "T \<in> measure_preserving P P"
 proof
   fix A :: "(nat \<Rightarrow> 'a) set" assume "A \<in> P.events"
   hence "emeasure P (T -` A \<inter> space P) = emeasure (distr P P T) A"
     by (subst emeasure_distr) simp_all
   also have "distr P P T = P" unfolding P_def T_def o_def
     using distr_PiM_reindex[of UNIV "\<lambda>_. M" Suc UNIV] by (simp add: prob_space_axioms restrict_def)
   finally show "emeasure P (T -` A \<inter> space P) = emeasure P A" .
 qed auto
 
 sublocale fmpt P T
   by unfold_locales
      (use measure_preserving in \<open>blast intro: measure_preserving_is_quasi_measure_preserving\<close>)+
 
 
-text \<open>
-  Related to the tail algebra, we define the algebra induced by the \<open>i\<close>-th variable (i.e.
-  the algebra that contains only information about the \<open>i\<close>-th variable):
-\<close>
-sublocale X: sigma_algebra "space P" "sets.pullback_algebra M (\<lambda>f. f i) (space P)"
-  by (rule sets.sigma_algebra_pullback)
-
-lemma indep_sets_pullback_algebra:
-  "P.indep_sets (\<lambda>i. sets.pullback_algebra M (\<lambda>f. f i) (space P)) UNIV"
-  using indep_vars unfolding P.indep_vars_def sets.pullback_algebra_def by blast
+lemma indep_sets_vimage_algebra:
+  "P.indep_sets (\<lambda>i. sets (vimage_algebra (space P) (\<lambda>f. f i) M)) UNIV"
+  using indep_vars unfolding P.indep_vars_def sets_vimage_algebra by blast
 
 
 text \<open>
   We can now show that the tail algebra $\mathcal{T}_n$ is a subalgebra of the algebra generated by the
   algebras induced by all the variables \<open>x\<^sub>i\<close> with \<open>i \<ge> n\<close>:
 \<close>
 lemma tail_algebra_subset:
   "sets (tail_algebra n) \<subseteq>
-     sigma_sets (space P) (\<Union>i\<in>{n..}. sets.pullback_algebra M (\<lambda>f. f i) (space P))"
+     sigma_sets (space P) (\<Union>i\<in>{n..}. sets (vimage_algebra (space P) (\<lambda>f. f i) M))"
 proof -
   have "sets (tail_algebra n) = sigma_sets (space P)
            (prod_algebra UNIV (\<lambda>i. if i < n then trivial_measure (space M) else M))"
     by (simp add: tail_algebra_def sets_PiM PiE_def Pi_def P_def space_PiM)
 
-  also have "\<dots> \<subseteq> sigma_sets (space P) (\<Union>i\<in>{n..}. sets.pullback_algebra M (\<lambda>f. f i) (space P))"
+  also have "\<dots> \<subseteq> sigma_sets (space P) (\<Union>i\<in>{n..}. sets (vimage_algebra (space P) (\<lambda>f. f i) M))"
   proof (intro sigma_sets_mono subsetI)
     fix C assume "C \<in> prod_algebra UNIV (\<lambda>i. if i < n then trivial_measure (space M) else M)"
     then obtain C'
       where C': "C = Pi\<^sub>E UNIV C'"
                 "C' \<in> (\<Pi> i\<in>UNIV. sets (if i < n then trivial_measure (space M) else M))"
       by (elim prod_algebraE_all)
     have C'_1: "C' i \<in> {{}, space M}" if "i < n" for i
       using C'(2) that by (auto simp: Pi_def sets_trivial_measure split: if_splits)
     have C'_2: "C' i \<in> sets M" if "i \<ge> n" for i
     proof -
       from that have "\<not>(i < n)"
         by auto
       with C'(2) show ?thesis
         by (force simp: Pi_def sets_trivial_measure split: if_splits)
     qed
     have "C' i \<in> events" for i
       using C'_1[of i] C'_2[of i] by (cases "i \<ge> n") auto
     hence "C \<in> sets P"
       unfolding P_def C'(1) by (intro sets_PiM_I_countable) auto
     hence "C \<subseteq> space P"
       using sets.sets_into_space by blast
 
-    show "C \<in> sigma_sets (space P) (\<Union>i\<in>{n..}. sets.pullback_algebra M (\<lambda>f. f i) (space P))"
+    show "C \<in> sigma_sets (space P) (\<Union>i\<in>{n..}. sets (vimage_algebra (space P) (\<lambda>f. f i) M))"
     proof (cases "C = {}")
       case False
       have "C = (\<Inter>i\<in>{n..}. (\<lambda>f. f i) -` C' i) \<inter> space P"
       proof (intro equalityI subsetI, goal_cases)
         case (1 f)
         hence "f \<in> space P"
           using 1 \<open>C \<subseteq> space P\<close> by blast
         thus ?case
           using C' 1 by (auto simp: Pi_def sets_trivial_measure split: if_splits)
       next
         case (2 f)
         hence f: "f i \<in> C' i" if "i \<ge> n" for i
           using that by auto
         have "f i \<in> C' i" for i
         proof (cases "i \<ge> n")
           case True
           thus ?thesis using C'_2[of i] f[of i] by auto
         next
           case False
           thus ?thesis using C'_1[of i] C'(1) \<open>C \<noteq> {}\<close> 2
             by (auto simp: P_def space_PiM)
         qed
         thus "f \<in> C"
           using C' by auto
       qed
 
       also have "(\<Inter>i\<in>{n..}. (\<lambda>f. f i) -` C' i) \<inter> space P =
                  (\<Inter>i\<in>{n..}. (\<lambda>f. f i) -` C' i \<inter> space P)"
         by blast
 
-      also have "\<dots> \<in> sigma_sets (space P) (\<Union>i\<in>{n..}. sets.pullback_algebra M (\<lambda>f. f i) (space P))"
+      also have "\<dots> \<in> sigma_sets (space P) (\<Union>i\<in>{n..}. sets (vimage_algebra (space P) (\<lambda>f. f i) M))"
         (is "_ \<in> ?rhs")
       proof (intro sigma_sets_INTER, goal_cases)
         fix i show "(\<lambda>f. f i) -` C' i \<inter> space P \<in> ?rhs"
         proof (cases "i \<ge> n")
           case False
           hence "C' i = {} \<or> C' i = space M"
             using C'_1[of i] by auto
           thus ?thesis
           proof
             assume [simp]: "C' i = space M"
             have "space P \<subseteq> (\<lambda>f. f i) -` C' i"
               by (auto simp: P_def space_PiM)
             hence "(\<lambda>f. f i) -` C' i \<inter> space P = space P"
               by blast
             thus ?thesis using sigma_sets_top
               by metis
           qed (auto intro: sigma_sets.Empty)
         next
           case i: True
-          have "(\<lambda>f. f i) -` C' i \<inter> space P \<in> sets.pullback_algebra M (\<lambda>f. f i) (space P)"
-            using C'_2[OF i] by (intro sets.in_pullback_algebra) auto
+          have "(\<lambda>f. f i) -` C' i \<inter> space P \<in> sets (vimage_algebra (space P) (\<lambda>f. f i) M)"
+            using C'_2[OF i] by (blast intro: in_vimage_algebra)
           thus ?thesis using i by blast
         qed
       next
-        have "C \<subseteq> space P" if "C \<in> sets.pullback_algebra M (\<lambda>f. f i) (space P)" for i C
-        proof -
-          show ?thesis
-            by (rule sigma_sets_into_sp) (use that X.space_closed[of i] in auto)
-        qed
-        thus "(\<Union>i\<in>{n..}. sets.pullback_algebra M (\<lambda>f. f i) (space P))\<subseteq> Pow (space P)"
+        have "C \<subseteq> space P" if "C \<in> sets (vimage_algebra (space P) (\<lambda>f. f i) M)" for i C
+          using sets.sets_into_space[OF that] by simp
+        thus "(\<Union>i\<in>{n..}. sets (vimage_algebra (space P) (\<lambda>f. f i) M)) \<subseteq> Pow (space P)"
           by auto
       qed auto
 
       finally show ?thesis .
     qed (auto simp: sigma_sets.Empty)
   qed
 
   finally show ?thesis .
 qed
 
 text \<open>
   It now follows that the \<open>T\<close>-invariant events are a subset of the tail algebra induced
   by the variables:
 \<close>
 lemma Invariants_subset_tail_algebra:
-  "sets Invariants \<subseteq> P.tail_events (\<lambda>i. sets.pullback_algebra M (\<lambda>f. f i) (space P))"
+  "sets Invariants \<subseteq> P.tail_events (\<lambda>i. sets (vimage_algebra (space P) (\<lambda>f. f i) M))"
 proof
   fix A assume A: "A \<in> sets Invariants"
   have A': "A \<in> P.events"
     using A unfolding Invariants_sets by simp_all
-  show "A \<in> P.tail_events (\<lambda>i. sets.pullback_algebra M (\<lambda>f. f i) (space P))"
+  show "A \<in> P.tail_events (\<lambda>i. sets (vimage_algebra (space P) (\<lambda>f. f i) M))"
         unfolding P.tail_events_def
   proof safe
     fix n :: nat
     have "vimage_restr T A = A"
       using A by (simp add: Invariants_vrestr)
     hence "A = vimage_restr (T ^^ n) A"
       using A' by (induction n) (simp_all add: vrestr_comp)
     also have "vimage_restr (T ^^ n) A = (T ^^ n) -` (A \<inter> space P) \<inter> space P"
       unfolding vimage_restr_def ..
     also have "A \<inter> space P = A"
       using A' by simp
     also have "space P = space (tail_algebra n)"
       by (simp add: P_def space_PiM)
     also have "(T ^^ n) -` A \<inter> space (tail_algebra n) \<in> sets (tail_algebra n)"
       by (rule measurable_sets[OF measurable_funpow_T' A'])
     also have "sets (tail_algebra n) \<subseteq>
-               sigma_sets (space P) (\<Union>i\<in>{n..}. sets.pullback_algebra M (\<lambda>f. f i) (space P))"
+               sigma_sets (space P) (\<Union>i\<in>{n..}. sets (vimage_algebra (space P) (\<lambda>f. f i) M))"
       by (rule tail_algebra_subset)
-    finally show "A \<in> sigma_sets (space P) (\<Union>i\<in>{n..}. sets.pullback_algebra M (\<lambda>f. f i) (space P))" .
+    finally show "A \<in> sigma_sets (space P)
+                        (\<Union>i\<in>{n..}. sets (vimage_algebra (space P) (\<lambda>f. f i) M))" .
   qed
 qed
 
 text \<open>
   A simple invocation of Kolmogorov's 0--1 law now proves that \<open>T\<close> is indeed ergodic:
 \<close>
 sublocale ergodic_fmpt P T
 proof
   fix A assume A: "A \<in> sets Invariants"
   have A': "A \<in> P.events"
     using A unfolding Invariants_sets by simp_all
-  have "P.prob A = 0 \<or> P.prob A = 1"
-    using X.sigma_algebra_axioms indep_sets_pullback_algebra
+  have "sigma_algebra (space P) (sets (vimage_algebra (space P) (\<lambda>f. f i) M))" for i
+    by (metis sets.sigma_algebra_axioms space_vimage_algebra)
+  hence "P.prob A = 0 \<or> P.prob A = 1"
+    using indep_sets_vimage_algebra
     by (rule P.kolmogorov_0_1_law) (use A Invariants_subset_tail_algebra in blast)
   thus "A \<in> null_sets P \<or> space P - A \<in> null_sets P"
     by (rule disj_forward) (use A'(1) P.prob_compl[of A] in \<open>auto simp: P.emeasure_eq_measure\<close>)
 qed
 
 end
 
 end
\ No newline at end of file