# HG changeset patch
# User haftmann
# Date 1617798499 0
# Node ID 5131c388a9b07c8a6e5249d65398b598074cf059
# Parent  0f33c7031ec94db434f6e6d96b4fc7d1f59b376d
simplified definition

diff -r 0f33c7031ec9 -r 5131c388a9b0 src/HOL/Analysis/Bochner_Integration.thy
--- a/src/HOL/Analysis/Bochner_Integration.thy	Tue Apr 06 18:12:20 2021 +0000
+++ b/src/HOL/Analysis/Bochner_Integration.thy	Wed Apr 07 12:28:19 2021 +0000
@@ -227,7 +227,7 @@
                    (\<Sum>y\<in>F. y * indicat_real {x \<in> space M. U' i x = y} z))"
         using insert(1-3)
         by (intro add * sum_nonneg mult_nonneg_nonneg)
-           (auto simp: nonneg indicator_def sum_nonneg_eq_0_iff)
+           (auto simp: nonneg indicator_def of_bool_def sum_nonneg_eq_0_iff)
       thus ?case 
         using insert.hyps by (subst sum.insert) auto
     qed
diff -r 0f33c7031ec9 -r 5131c388a9b0 src/HOL/Analysis/Borel_Space.thy
--- a/src/HOL/Analysis/Borel_Space.thy	Tue Apr 06 18:12:20 2021 +0000
+++ b/src/HOL/Analysis/Borel_Space.thy	Wed Apr 07 12:28:19 2021 +0000
@@ -313,7 +313,7 @@
   shows "f \<in> borel_measurable (restrict_space M \<Omega>) \<longleftrightarrow>
     (\<lambda>x. f x * indicator \<Omega> x) \<in> borel_measurable M"
   by (subst measurable_restrict_space_iff)
-     (auto simp: indicator_def if_distrib[where f="\<lambda>x. a * x" for a] cong del: if_weak_cong)
+     (auto simp: indicator_def of_bool_def if_distrib[where f="\<lambda>x. a * x" for a] cong del: if_weak_cong)
 
 lemma borel_measurable_restrict_space_iff_ennreal:
   fixes f :: "'a \<Rightarrow> ennreal"
@@ -321,7 +321,7 @@
   shows "f \<in> borel_measurable (restrict_space M \<Omega>) \<longleftrightarrow>
     (\<lambda>x. f x * indicator \<Omega> x) \<in> borel_measurable M"
   by (subst measurable_restrict_space_iff)
-     (auto simp: indicator_def if_distrib[where f="\<lambda>x. a * x" for a] cong del: if_weak_cong)
+     (auto simp: indicator_def of_bool_def if_distrib[where f="\<lambda>x. a * x" for a] cong del: if_weak_cong)
 
 lemma borel_measurable_restrict_space_iff:
   fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
@@ -329,7 +329,7 @@
   shows "f \<in> borel_measurable (restrict_space M \<Omega>) \<longleftrightarrow>
     (\<lambda>x. indicator \<Omega> x *\<^sub>R f x) \<in> borel_measurable M"
   by (subst measurable_restrict_space_iff)
-     (auto simp: indicator_def if_distrib[where f="\<lambda>x. x *\<^sub>R a" for a] ac_simps
+     (auto simp: indicator_def of_bool_def if_distrib[where f="\<lambda>x. x *\<^sub>R a" for a] ac_simps
        cong del: if_weak_cong)
 
 lemma cbox_borel[measurable]: "cbox a b \<in> sets borel"
diff -r 0f33c7031ec9 -r 5131c388a9b0 src/HOL/Analysis/Change_Of_Vars.thy
--- a/src/HOL/Analysis/Change_Of_Vars.thy	Tue Apr 06 18:12:20 2021 +0000
+++ b/src/HOL/Analysis/Change_Of_Vars.thy	Wed Apr 07 12:28:19 2021 +0000
@@ -2385,7 +2385,7 @@
       ultimately show ?thesis
         using \<open>y > 0\<close> integral_restrict_Int [of S "{t. h n (g t) = y}" "\<lambda>t. \<bar>det (matrix (g' t))\<bar> * y"]
         apply (simp add: integrable_on_indicator integral_indicator)
-        apply (simp add: indicator_def if_distrib cong: if_cong)
+        apply (simp add: indicator_def of_bool_def if_distrib cong: if_cong)
         done
     qed
     have hn_int: "h n integrable_on g ` S"
@@ -2415,7 +2415,7 @@
           fix x
           assume "x \<in> S"
           have "y * indicat_real {x. h n x = y} (g x) \<le> f (g x)"
-            by (metis (full_types) \<open>x \<in> S\<close> h_le_f indicator_def mem_Collect_eq mult.right_neutral mult_zero_right nonneg_fg)
+            by (metis \<open>x \<in> S\<close> h_le_f indicator_simps(1) indicator_simps(2) mem_Collect_eq mult.commute mult.left_neutral mult_zero_left nonneg_fg)
           with \<open>y \<ge> 0\<close> show "norm (?D x * y * indicat_real {x. h n x = y} (g x)) \<le> ?D x * f(g x)"
             by (simp add: abs_mult mult.assoc mult_left_mono)
         qed (use S det_int_fg in auto)
@@ -2867,7 +2867,7 @@
               = (if x \<in> T then 1 else 0) * f x" for x
         by auto
       show "f absolutely_integrable_on T"
-        using fa by (simp add: indicator_def set_integrable_def eq)
+        using fa by (simp add: indicator_def of_bool_def set_integrable_def eq)
       have [simp]: "{y \<in> T. f y < 0} \<inter> {y \<in> T. 0 < f y} = {}" for T and f :: "(real^'n::_) \<Rightarrow> real"
         by auto
       have "integral T f = integral ({y \<in> T. f y < 0} \<union> {y \<in> T. f y > 0}) f"
@@ -2929,7 +2929,7 @@
       have "?DP absolutely_integrable_on ({x \<in> S. f (g x) < 0} \<union> {x \<in> S. f (g x) > 0})"
         by (rule absolutely_integrable_Un [OF aDN aDP])
       then show I: "?DP absolutely_integrable_on S"
-        by (simp add: indicator_def eq set_integrable_def)
+        by (simp add: indicator_def of_bool_def eq set_integrable_def)
       have [simp]: "{y \<in> S. f y < 0} \<inter> {y \<in> S. 0 < f y} = {}" for S and f :: "(real^'n::_) \<Rightarrow> real"
         by auto
       have "integral S ?DP = integral ({x \<in> S. f (g x) < 0} \<union> {x \<in> S. f (g x) > 0}) ?DP"
diff -r 0f33c7031ec9 -r 5131c388a9b0 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Tue Apr 06 18:12:20 2021 +0000
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Wed Apr 07 12:28:19 2021 +0000
@@ -433,7 +433,7 @@
       moreover have "(\<lambda>k. indicator (A \<inter> ?B k) x :: real) \<longlonglongrightarrow> indicator (\<Union>k::nat. A \<inter> ?B k) x"
         by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def box_def)
       ultimately show "(\<lambda>k. if x \<in> A \<inter> ?B k then 1 else 0::real) \<longlonglongrightarrow> 1"
-        by (simp add: indicator_def UN_box_eq_UNIV) }
+        by (simp add: indicator_def of_bool_def UN_box_eq_UNIV) }
 
     have "(\<lambda>n. emeasure lborel (A \<inter> ?B n)) \<longlonglongrightarrow> emeasure lborel (\<Union>n::nat. A \<inter> ?B n)"
       by (intro Lim_emeasure_incseq) (auto simp: incseq_def box_def)
@@ -459,7 +459,7 @@
   then have "((\<lambda>x. 1) has_integral measure lborel A) A"
     by (intro has_integral_measure_lborel) (auto simp: ennreal_indicator)
   with set show ?case
-    by (simp add: ennreal_indicator measure_def) (simp add: indicator_def)
+    by (simp add: ennreal_indicator measure_def) (simp add: indicator_def of_bool_def)
 next
   case (mult g c)
   then have "ennreal c * (\<integral>\<^sup>+ x. g x \<partial>lborel) = ennreal r"
@@ -626,7 +626,7 @@
   proof
     assume int: "(\<lambda>x. 1::real) integrable_on A"
     then have "(indicator A::'a \<Rightarrow> real) integrable_on UNIV"
-      unfolding indicator_def[abs_def] integrable_restrict_UNIV .
+      unfolding indicator_def of_bool_def integrable_restrict_UNIV .
     then obtain r where "((indicator A::'a\<Rightarrow>real) has_integral r) UNIV"
       by auto
     from nn_integral_has_integral_lborel[OF _ _ this] emeasure_A show False
@@ -706,7 +706,7 @@
     by (auto dest: completion_ex_borel_measurable_real)
 
   from I have "((\<lambda>x. abs (indicator \<Omega> x * f x)) has_integral I) UNIV"
-    using nonneg by (simp add: indicator_def if_distrib[of "\<lambda>x. x * f y" for y] cong: if_cong)
+    using nonneg by (simp add: indicator_def of_bool_def if_distrib[of "\<lambda>x. x * f y" for y] cong: if_cong)
   also have "((\<lambda>x. abs (indicator \<Omega> x * f x)) has_integral I) UNIV \<longleftrightarrow> ((\<lambda>x. abs (f' x)) has_integral I) UNIV"
     using eq by (intro has_integral_AE) auto
   finally have "integral\<^sup>N lborel (\<lambda>x. abs (f' x)) = I"
@@ -915,7 +915,8 @@
   assumes f: "set_integrable lebesgue S f"
   shows "(f has_integral (LINT x:S|lebesgue. f x)) S"
   using has_integral_integral_lebesgue f
-  by (fastforce simp add: set_integrable_def set_lebesgue_integral_def indicator_def if_distrib[of "\<lambda>x. x *\<^sub>R f _"] cong: if_cong)
+  by (fastforce simp add: set_integrable_def set_lebesgue_integral_def indicator_def
+    of_bool_def if_distrib[of "\<lambda>x. x *\<^sub>R f _"] cong: if_cong)
 
 lemma set_lebesgue_integral_eq_integral:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
@@ -1145,7 +1146,7 @@
   by (simp add: lmeasurable_iff_has_integral integral_unique)
 
 lemma lmeasure_integral: "S \<in> lmeasurable \<Longrightarrow> measure lebesgue S = integral S (\<lambda>x. 1::real)"
-  by (fastforce simp add: lmeasure_integral_UNIV indicator_def[abs_def] lmeasurable_iff_integrable_on)
+  by (fastforce simp add: lmeasure_integral_UNIV indicator_def [abs_def] of_bool_def lmeasurable_iff_integrable_on)
 
 lemma integrable_on_const: "S \<in> lmeasurable \<Longrightarrow> (\<lambda>x. c) integrable_on S"
   unfolding lmeasurable_iff_integrable
@@ -1156,7 +1157,7 @@
   shows "integral T (indicator S) = measure lebesgue (S \<inter> T)"
 proof -
   have "integral UNIV (indicator (S \<inter> T)) = integral UNIV (\<lambda>a. if a \<in> S \<inter> T then 1::real else 0)"
-    by (meson indicator_def)
+    by (simp add: indicator_def [abs_def] of_bool_def)
   moreover have "(indicator (S \<inter> T) has_integral measure lebesgue (S \<inter> T)) UNIV"
     using assms by (simp add: lmeasurable_iff_has_integral)
   ultimately have "integral UNIV (\<lambda>x. if x \<in> S \<inter> T then 1 else 0) = measure lebesgue (S \<inter> T)"
@@ -1164,7 +1165,7 @@
   moreover have "integral T (\<lambda>a. if a \<in> S then 1::real else 0) = integral (S \<inter> T \<inter> UNIV) (\<lambda>a. 1)"
     by (simp add: Henstock_Kurzweil_Integration.integral_restrict_Int)
   moreover have "integral T (indicat_real S) = integral T (\<lambda>a. if a \<in> S then 1 else 0)"
-    by (meson indicator_def)
+    by (simp add: indicator_def [abs_def] of_bool_def)
   ultimately show ?thesis
     by (simp add: assms lmeasure_integral)
 qed
@@ -1563,7 +1564,7 @@
     and 1: "(indicat_real (\<Union>m\<le>k. S m)) integrable_on UNIV" for k
     by (auto simp: negligible has_integral_iff)
   have 2: "\<And>k x. indicat_real (\<Union>m\<le>k. S m) x \<le> (indicat_real (\<Union>m\<le>Suc k. S m) x)"
-    by (simp add: indicator_def)
+    by (auto simp add: indicator_def)
   have 3: "\<And>x. (\<lambda>k. indicat_real (\<Union>m\<le>k. S m) x) \<longlonglongrightarrow> (indicat_real (\<Union>n. S n) x)"
     by (force simp: indicator_def eventually_sequentially intro: tendsto_eventually)
   have 4: "bounded (range (\<lambda>k. integral UNIV (indicat_real (\<Union>m\<le>k. S m))))"
@@ -3832,7 +3833,7 @@
        (auto simp: has_field_derivative_iff_has_vector_derivative[symmetric]
              intro: has_field_derivative_subset[OF f(1)] \<open>a \<le> b\<close>)
   then have i: "((\<lambda>x. f x * indicator {a .. b} x) has_integral F b - F a) UNIV"
-    unfolding indicator_def if_distrib[where f="\<lambda>x. a * x" for a]
+    unfolding indicator_def of_bool_def if_distrib[where f="\<lambda>x. a * x" for a]
     by (simp cong del: if_weak_cong del: atLeastAtMost_iff)
   then have nn: "(\<integral>\<^sup>+x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a"
     by (rule nn_integral_has_integral_lborel[OF *])
@@ -3862,7 +3863,7 @@
   moreover
   have "(f has_integral integral\<^sup>L lborel ?f) {a..b}"
     using has_integral_integral_lborel[OF int]
-    unfolding indicator_def if_distrib[where f="\<lambda>x. x *\<^sub>R a" for a]
+    unfolding indicator_def of_bool_def if_distrib[where f="\<lambda>x. x *\<^sub>R a" for a]
     by (simp cong del: if_weak_cong del: atLeastAtMost_iff)
   ultimately show ?eq
     by (auto dest: has_integral_unique)
diff -r 0f33c7031ec9 -r 5131c388a9b0 src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy
--- a/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy	Tue Apr 06 18:12:20 2021 +0000
+++ b/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy	Wed Apr 07 12:28:19 2021 +0000
@@ -881,7 +881,7 @@
     finally have le: "emeasure lebesgue (-T \<inter> U) < ennreal (1 / 2^n)"
       by (simp add: eq)
     have 1: "continuous_on (T \<union> -U) (indicat_real S)"
-      unfolding indicator_def
+      unfolding indicator_def of_bool_def
     proof (rule continuous_on_cases [OF \<open>closed T\<close>])
       show "closed (- U)"
         using \<open>open U\<close> by blast
@@ -976,7 +976,7 @@
     using nn
     by (auto simp: inj_on_def intro: sum.cong)
   finally show ?thesis
-    by (subst *) (simp add: enn2real_sum indicator_def if_distrib cong: if_cong)
+    by (subst *) (simp add: enn2real_sum indicator_def of_bool_def if_distrib cong: if_cong)
 qed
 
 lemma\<^marker>\<open>tag important\<close> simple_function_induct_real
diff -r 0f33c7031ec9 -r 5131c388a9b0 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Apr 06 18:12:20 2021 +0000
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Apr 07 12:28:19 2021 +0000
@@ -2336,7 +2336,7 @@
       and  "(indicat_real T has_integral 0) (cbox a b)" for a b
   proof (subst has_integral_spike_eq[OF T])
     show "indicat_real S x = indicat_real (S \<union> T) x" if "x \<in> cbox a b - T" for x
-      by (metis Diff_iff Un_iff indicator_def that)
+      using that by (simp add: indicator_def)
     show "(indicat_real S has_integral 0) (cbox a b)"
       by (simp add: S0)
   qed
diff -r 0f33c7031ec9 -r 5131c388a9b0 src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Tue Apr 06 18:12:20 2021 +0000
+++ b/src/HOL/Analysis/Measure_Space.thy	Wed Apr 07 12:28:19 2021 +0000
@@ -49,9 +49,8 @@
   have "P \<inter> {i. x \<in> A i} = {j}"
     using d \<open>x \<in> A j\<close> \<open>j \<in> P\<close> unfolding disjoint_family_on_def
     by auto
-  thus ?thesis
-    unfolding indicator_def
-    by (simp add: if_distrib sum.If_cases[OF \<open>finite P\<close>])
+  with \<open>finite P\<close> show ?thesis
+    by (simp add: indicator_def)
 qed
 
 text \<open>
diff -r 0f33c7031ec9 -r 5131c388a9b0 src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Tue Apr 06 18:12:20 2021 +0000
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Wed Apr 07 12:28:19 2021 +0000
@@ -1809,7 +1809,7 @@
   have *: "(\<integral>\<^sup>+x. max 0 (f x) \<partial>count_space A) =
     (\<integral>\<^sup>+ x. (\<Sum>a|a\<in>A \<and> 0 < f a. f a * indicator {a} x) \<partial>count_space A)"
     by (auto intro!: nn_integral_cong
-             simp add: indicator_def if_distrib sum.If_cases[OF A] max_def le_less)
+             simp add: indicator_def of_bool_def if_distrib sum.If_cases[OF A] max_def le_less)
   also have "\<dots> = (\<Sum>a|a\<in>A \<and> 0 < f a. \<integral>\<^sup>+ x. f a * indicator {a} x \<partial>count_space A)"
     by (subst nn_integral_sum) (simp_all add: AE_count_space  less_imp_le)
   also have "\<dots> = (\<Sum>a|a\<in>A \<and> 0 < f a. f a)"
@@ -2451,7 +2451,7 @@
   have "{a. (a \<in> X \<longrightarrow> a \<in> A \<and> 0 < f a) \<and> a \<in> X} = {a\<in>X. 0 < f a}"
     using \<open>X \<subseteq> A\<close> by auto
   with A show ?thesis
-    by (simp add: emeasure_density nn_integral_count_space point_measure_def indicator_def)
+    by (simp add: emeasure_density nn_integral_count_space point_measure_def indicator_def of_bool_def)
 qed
 
 lemma emeasure_point_measure_finite:
diff -r 0f33c7031ec9 -r 5131c388a9b0 src/HOL/Analysis/Set_Integral.thy
--- a/src/HOL/Analysis/Set_Integral.thy	Tue Apr 06 18:12:20 2021 +0000
+++ b/src/HOL/Analysis/Set_Integral.thy	Wed Apr 07 12:28:19 2021 +0000
@@ -59,7 +59,7 @@
   shows   "set_integrable M A f = set_integrable M' A' f'"
 proof -
   have "(\<lambda>x. indicator A x *\<^sub>R f x) = (\<lambda>x. indicator A' x *\<^sub>R f' x)"
-    using assms by (auto simp: indicator_def)
+    using assms by (auto simp: indicator_def of_bool_def)
   thus ?thesis by (simp add: set_integrable_def assms)
 qed
 
@@ -652,13 +652,11 @@
   assumes "A \<in> sets M" "B \<in> sets M"
           "(A - B) \<union> (B - A) \<in> null_sets M"
   shows "(\<integral>\<^sup>+x \<in> A. f x \<partial>M) = (\<integral>\<^sup>+x \<in> B. f x \<partial>M)"
-proof (rule nn_integral_cong_AE, auto simp add: indicator_def)
+proof (rule nn_integral_cong_AE)
   have *: "AE a in M. a \<notin> (A - B) \<union> (B - A)"
     using assms(3) AE_not_in by blast
-  then show "AE a in M. a \<notin> A \<longrightarrow> a \<in> B \<longrightarrow> f a = 0"
+  then show \<open>AE x in M. f x * indicator A x = f x * indicator B x\<close>
     by auto
-  show "AE x\<in>A in M. x \<notin> B \<longrightarrow> f x = 0"
-    using * by auto
 qed
 
 proposition nn_integral_disjoint_family:
diff -r 0f33c7031ec9 -r 5131c388a9b0 src/HOL/Library/Indicator_Function.thy
--- a/src/HOL/Library/Indicator_Function.thy	Tue Apr 06 18:12:20 2021 +0000
+++ b/src/HOL/Library/Indicator_Function.thy	Wed Apr 07 12:28:19 2021 +0000
@@ -8,7 +8,7 @@
 imports Complex_Main Disjoint_Sets
 begin
 
-definition "indicator S x = (if x \<in> S then 1 else 0)"
+definition "indicator S x = of_bool (x \<in> S)"
 
 text\<open>Type constrained version\<close>
 abbreviation indicat_real :: "'a set \<Rightarrow> 'a \<Rightarrow> real" where "indicat_real S \<equiv> indicator S"
@@ -98,7 +98,7 @@
 
 lemma LIMSEQ_indicator_incseq:
   assumes "incseq A"
-  shows "(\<lambda>i. indicator (A i) x :: 'a::{topological_space,one,zero}) \<longlonglongrightarrow> indicator (\<Union>i. A i) x"
+  shows "(\<lambda>i. indicator (A i) x :: 'a::{topological_space,zero_neq_one}) \<longlonglongrightarrow> indicator (\<Union>i. A i) x"
 proof (cases "\<exists>i. x \<in> A i")
   case True
   then obtain i where "x \<in> A i"
@@ -115,7 +115,7 @@
 qed
 
 lemma LIMSEQ_indicator_UN:
-  "(\<lambda>k. indicator (\<Union>i<k. A i) x :: 'a::{topological_space,one,zero}) \<longlonglongrightarrow> indicator (\<Union>i. A i) x"
+  "(\<lambda>k. indicator (\<Union>i<k. A i) x :: 'a::{topological_space,zero_neq_one}) \<longlonglongrightarrow> indicator (\<Union>i. A i) x"
 proof -
   have "(\<lambda>k. indicator (\<Union>i<k. A i) x::'a) \<longlonglongrightarrow> indicator (\<Union>k. \<Union>i<k. A i) x"
     by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def intro: less_le_trans)
@@ -126,7 +126,7 @@
 
 lemma LIMSEQ_indicator_decseq:
   assumes "decseq A"
-  shows "(\<lambda>i. indicator (A i) x :: 'a::{topological_space,one,zero}) \<longlonglongrightarrow> indicator (\<Inter>i. A i) x"
+  shows "(\<lambda>i. indicator (A i) x :: 'a::{topological_space,zero_neq_one}) \<longlonglongrightarrow> indicator (\<Inter>i. A i) x"
 proof (cases "\<exists>i. x \<notin> A i")
   case True
   then obtain i where "x \<notin> A i"
@@ -143,7 +143,7 @@
 qed
 
 lemma LIMSEQ_indicator_INT:
-  "(\<lambda>k. indicator (\<Inter>i<k. A i) x :: 'a::{topological_space,one,zero}) \<longlonglongrightarrow> indicator (\<Inter>i. A i) x"
+  "(\<lambda>k. indicator (\<Inter>i<k. A i) x :: 'a::{topological_space,zero_neq_one}) \<longlonglongrightarrow> indicator (\<Inter>i. A i) x"
 proof -
   have "(\<lambda>k. indicator (\<Inter>i<k. A i) x::'a) \<longlonglongrightarrow> indicator (\<Inter>k. \<Inter>i<k. A i) x"
     by (intro LIMSEQ_indicator_decseq) (auto simp: decseq_def intro: less_le_trans)
diff -r 0f33c7031ec9 -r 5131c388a9b0 src/HOL/Probability/Product_PMF.thy
--- a/src/HOL/Probability/Product_PMF.thy	Tue Apr 06 18:12:20 2021 +0000
+++ b/src/HOL/Probability/Product_PMF.thy	Wed Apr 07 12:28:19 2021 +0000
@@ -341,7 +341,7 @@
 lemma Pi_pmf_return_pmf [simp]:
   assumes "finite A"
   shows   "Pi_pmf A dflt (\<lambda>x. return_pmf (f x)) = return_pmf (\<lambda>x. if x \<in> A then f x else dflt)"
-  using assms by (intro pmf_eqI) (auto simp: pmf_Pi simp: indicator_def)
+  using assms by (intro pmf_eqI) (auto simp: pmf_Pi simp: indicator_def split: if_splits)
 
 text \<open>
   Analogously any componentwise mapping can be pulled outside the product: