--- 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
--- 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"
--- 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"
--- 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)
--- 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
--- 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
--- 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>
--- 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:
--- 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:
--- 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)
--- 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: