--- a/NEWS Wed Feb 14 16:25:41 2024 +0100
+++ b/NEWS Thu Feb 15 08:25:25 2024 +0100
@@ -25,6 +25,9 @@
by Sledgehammer and should be used instead. For more information, see
Sledgehammer's documentation relating to "preplay_timeout". INCOMPATIBILITY.
+* HOL-Analysis: the syntax of Lebesgue integrals (LINT, LBINT, \<integral>, etc.) now
+ requires parentheses in most cases. INCOMPATIBILITY.
+
* HOL-Analysis: corrected the definition of convex function (convex_on)
to require the underlying set to be convex. INCOMPATIBILITY.
--- a/etc/build.props Wed Feb 14 16:25:41 2024 +0100
+++ b/etc/build.props Thu Feb 15 08:25:25 2024 +0100
@@ -68,6 +68,7 @@
src/Pure/Concurrent/future.scala \
src/Pure/Concurrent/isabelle_thread.scala \
src/Pure/Concurrent/mailbox.scala \
+ src/Pure/Concurrent/multithreading.scala \
src/Pure/Concurrent/par_list.scala \
src/Pure/Concurrent/synchronized.scala \
src/Pure/GUI/color_value.scala \
--- a/src/HOL/Analysis/Bochner_Integration.thy Wed Feb 14 16:25:41 2024 +0100
+++ b/src/HOL/Analysis/Bochner_Integration.thy Thu Feb 15 08:25:25 2024 +0100
@@ -1503,7 +1503,7 @@
proof (intro nn_integral_mono_AE, eventually_elim)
fix x assume "\<forall>i. norm (s i x) \<le> w x" "(\<lambda>i. s i x) \<longlonglongrightarrow> f x" "0 \<le> w x"
then show "ennreal (norm (f x)) \<le> ennreal (w x)"
- by (intro LIMSEQ_le_const2[where X="\<lambda>i. ennreal (norm (s i x))"]) (auto intro: tendsto_intros)
+ by (metis LIMSEQ_le_const2 ennreal_leI tendsto_norm)
qed
with w show "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) < \<infinity>" by auto
qed fact
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Wed Feb 14 16:25:41 2024 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Thu Feb 15 08:25:25 2024 +0100
@@ -927,10 +927,10 @@
lemma set_borel_integral_eq_integral:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "set_integrable lborel S f"
- shows "f integrable_on S" "LINT x : S | lborel. f x = integral S f"
+ shows "f integrable_on S" "(LINT x : S | lborel. f x) = integral S f"
proof -
let ?f = "\<lambda>x. indicator S x *\<^sub>R f x"
- have "(?f has_integral LINT x : S | lborel. f x) UNIV"
+ have "(?f has_integral (LINT x : S | lborel. f x)) UNIV"
using assms has_integral_integral_lborel
unfolding set_integrable_def set_lebesgue_integral_def by blast
hence 1: "(f has_integral (set_lebesgue_integral lborel S f)) S"
@@ -939,7 +939,7 @@
by (auto simp add: integrable_on_def)
with 1 have "(f has_integral (integral S f)) S"
by (intro integrable_integral, auto simp add: integrable_on_def)
- thus "LINT x : S | lborel. f x = integral S f"
+ thus "(LINT x : S | lborel. f x) = integral S f"
by (intro has_integral_unique [OF 1])
qed
@@ -954,7 +954,7 @@
lemma set_lebesgue_integral_eq_integral:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes f: "set_integrable lebesgue S f"
- shows "f integrable_on S" "LINT x:S | lebesgue. f x = integral S f"
+ shows "f integrable_on S" "(LINT x:S | lebesgue. f x) = integral S f"
using has_integral_set_lebesgue[OF f] by (auto simp: integral_unique integrable_on_def)
lemma lmeasurable_iff_has_integral:
@@ -2184,7 +2184,7 @@
lemma set_integral_norm_bound:
fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
- shows "set_integrable M k f \<Longrightarrow> norm (LINT x:k|M. f x) \<le> LINT x:k|M. norm (f x)"
+ shows "set_integrable M k f \<Longrightarrow> norm (LINT x:k|M. f x) \<le> (LINT x:k|M. norm (f x))"
using integral_norm_bound[of M "\<lambda>x. indicator k x *\<^sub>R f x"] by (simp add: set_lebesgue_integral_def)
lemma set_integral_finite_UN_AE:
@@ -2193,7 +2193,7 @@
and ae: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> AE x in M. (x \<in> A i \<and> x \<in> A j) \<longrightarrow> i = j"
and [measurable]: "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
and f: "\<And>i. i \<in> I \<Longrightarrow> set_integrable M (A i) f"
- shows "LINT x:(\<Union>i\<in>I. A i)|M. f x = (\<Sum>i\<in>I. LINT x:A i|M. f x)"
+ shows "(LINT x:(\<Union>i\<in>I. A i)|M. f x) = (\<Sum>i\<in>I. LINT x:A i|M. f x)"
using \<open>finite I\<close> order_refl[of I]
proof (induction I rule: finite_subset_induct')
case (insert i I')
@@ -4000,7 +4000,7 @@
= F b * G b - F a * G a - \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel"
proof-
have "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel)
- = LBINT x. F x * g x * indicat_real {a..b} x + f x * G x * indicat_real {a..b} x"
+ = (LBINT x. F x * g x * indicat_real {a..b} x + f x * G x * indicat_real {a..b} x)"
by (meson vector_space_over_itself.scale_left_distrib)
also have "... = (\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel) + \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel"
proof (intro Bochner_Integration.integral_add borel_integrable_atLeastAtMost cont_f cont_g continuous_intros)
--- a/src/HOL/Analysis/Interval_Integral.thy Wed Feb 14 16:25:41 2024 +0100
+++ b/src/HOL/Analysis/Interval_Integral.thy Thu Feb 15 08:25:25 2024 +0100
@@ -290,7 +290,7 @@
split: if_split_asm)
next
case (le a b)
- have "LBINT x:{x. - x \<in> einterval a b}. f (- x) = LBINT x:einterval (- b) (- a). f (- x)"
+ have "(LBINT x:{x. - x \<in> einterval a b}. f (- x)) = (LBINT x:einterval (- b) (- a). f (- x))"
unfolding interval_lebesgue_integrable_def set_lebesgue_integral_def einterval_def
by (metis (lifting) ereal_less_uminus_reorder ereal_uminus_less_reorder indicator_simps mem_Collect_eq uminus_ereal.simps(1))
then show ?case
@@ -315,13 +315,13 @@
lemma interval_integral_zero [simp]:
fixes a b :: ereal
- shows "LBINT x=a..b. 0 = 0"
+ shows "(LBINT x=a..b. 0) = 0"
unfolding interval_lebesgue_integral_def set_lebesgue_integral_def einterval_eq
by simp
lemma interval_integral_const [intro, simp]:
fixes a b c :: real
- shows "interval_lebesgue_integrable lborel a b (\<lambda>x. c)" and "LBINT x=a..b. c = c * (b - a)"
+ shows "interval_lebesgue_integrable lborel a b (\<lambda>x. c)" and "(LBINT x=a..b. c) = c * (b - a)"
unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def einterval_eq
by (auto simp: less_imp_le field_simps measure_def set_integrable_def set_lebesgue_integral_def)
@@ -780,7 +780,7 @@
and derivg: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (g has_real_derivative (g' x)) (at x within {a..b})"
and contf : "continuous_on (g ` {a..b}) f"
and contg': "continuous_on {a..b} g'"
- shows "LBINT x=a..b. g' x *\<^sub>R f (g x) = LBINT y=g a..g b. f y"
+ shows "(LBINT x=a..b. g' x *\<^sub>R f (g x)) = (LBINT y=g a..g b. f y)"
proof-
have v_derivg: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (g has_vector_derivative (g' x)) (at x within {a..b})"
using derivg unfolding has_real_derivative_iff_has_vector_derivative .
@@ -798,7 +798,7 @@
by (blast intro: continuous_on_compose2 contf contg)
have "continuous_on {a..b} (\<lambda>x. g' x *\<^sub>R f (g x))"
by (auto intro!: continuous_on_scaleR contg' contfg)
- then have "LBINT x. indicat_real {a..b} x *\<^sub>R g' x *\<^sub>R f (g x) = F (g b) - F (g a)"
+ then have "(LBINT x. indicat_real {a..b} x *\<^sub>R g' x *\<^sub>R f (g x)) = F (g b) - F (g a)"
using integral_FTC_atLeastAtMost [OF \<open>a \<le> b\<close> vector_diff_chain_within[OF v_derivg derivF]]
by force
then have "LBINT x=a..b. g' x *\<^sub>R f (g x) = F (g b) - F (g a)"
--- a/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy Wed Feb 14 16:25:41 2024 +0100
+++ b/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy Thu Feb 15 08:25:25 2024 +0100
@@ -78,12 +78,12 @@
using set_integrable_subset borel_integrable_atLeastAtMost'[OF contg']
by (metis \<open>{u'..v'} \<subseteq> {a..b}\<close> eucl_ivals(5) set_integrable_def sets_lborel u'v'(1))
hence "(\<integral>\<^sup>+x. ennreal (g' x) * indicator ({a..b} \<inter> g-` {u..v}) x \<partial>lborel) =
- LBINT x:{a..b} \<inter> g-`{u..v}. g' x"
+ (LBINT x:{a..b} \<inter> g-`{u..v}. g' x)"
unfolding set_lebesgue_integral_def
by (subst nn_integral_eq_integral[symmetric])
(auto intro!: derivg_nonneg nn_integral_cong split: split_indicator)
also from interval_integral_FTC_finite[OF A B]
- have "LBINT x:{a..b} \<inter> g-`{u..v}. g' x = v - u"
+ have "(LBINT x:{a..b} \<inter> g-`{u..v}. g' x) = v - u"
by (simp add: u'v' interval_integral_Icc \<open>u \<le> v\<close>)
finally have "(\<integral>\<^sup>+ x. ennreal (g' x) * indicator ({a..b} \<inter> g -` {u..v}) x \<partial>lborel) =
ennreal (v - u)" .
@@ -130,12 +130,12 @@
(simp split: split_indicator)
also have "... = \<integral>\<^sup>+ x. indicator (g-`A \<inter> {a..b}) x * ennreal (g' x * indicator {a..b} x) \<partial>lborel" (is "_ = ?I")
by (subst compl.IH, intro nn_integral_cong) (simp split: split_indicator)
- also have "g b - g a = LBINT x:{a..b}. g' x" using derivg'
+ also have "g b - g a = (LBINT x:{a..b}. g' x)" using derivg'
unfolding set_lebesgue_integral_def
by (intro integral_FTC_atLeastAtMost[symmetric])
(auto intro: continuous_on_subset[OF contg'] has_field_derivative_subset[OF derivg]
has_vector_derivative_at_within)
- also have "ennreal ... = \<integral>\<^sup>+ x. g' x * indicator {a..b} x \<partial>lborel"
+ also have "ennreal ... = (\<integral>\<^sup>+ x. g' x * indicator {a..b} x \<partial>lborel)"
using borel_integrable_atLeastAtMost'[OF contg'] unfolding set_lebesgue_integral_def
by (subst nn_integral_eq_integral)
(simp_all add: mult.commute derivg_nonneg set_integrable_def split: split_indicator)
@@ -341,7 +341,7 @@
from integrable have M2: "(\<lambda>x. -f x * indicator {g a..g b} x) \<in> borel_measurable borel"
by (force simp: mult.commute set_integrable_def)
- have "LBINT x. (f x :: real) * indicator {g a..g b} x =
+ have "(LBINT x. (f x :: real) * indicator {g a..g b} x) =
enn2real (\<integral>\<^sup>+ x. ennreal (f x) * indicator {g a..g b} x \<partial>lborel) -
enn2real (\<integral>\<^sup>+ x. ennreal (- (f x)) * indicator {g a..g b} x \<partial>lborel)" using integrable
unfolding set_integrable_def
--- a/src/HOL/Analysis/Set_Integral.thy Wed Feb 14 16:25:41 2024 +0100
+++ b/src/HOL/Analysis/Set_Integral.thy Thu Feb 15 08:25:25 2024 +0100
@@ -23,7 +23,7 @@
syntax
"_ascii_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
- ("(4LINT (_):(_)/|(_)./ _)" [0,60,110,61] 60)
+ ("(4LINT (_):(_)/|(_)./ _)" [0,60,110,61] 10)
translations
"LINT x:A|M. f" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
@@ -39,11 +39,11 @@
syntax
"_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real"
- ("(2LBINT _./ _)" [0,60] 60)
+ ("(2LBINT _./ _)" [0,60] 10)
syntax
"_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> real"
- ("(3LBINT _:_./ _)" [0,60,61] 60)
+ ("(3LBINT _:_./ _)" [0,60,61] 10)
(*
Basic properties
@@ -105,7 +105,7 @@
lemma set_lebesgue_integral_cong_AE:
assumes [measurable]: "A \<in> sets M" "f \<in> borel_measurable M" "g \<in> borel_measurable M"
assumes "AE x \<in> A in M. f x = g x"
- shows "LINT x:A|M. f x = LINT x:A|M. g x"
+ shows "(LINT x:A|M. f x) = (LINT x:A|M. g x)"
proof-
have "AE x in M. indicator A x *\<^sub>R f x = indicator A x *\<^sub>R g x"
using assms by auto
@@ -149,25 +149,25 @@
(* TODO: integral_cmul_indicator should be named set_integral_const *)
(* TODO: borel_integrable_atLeastAtMost should be named something like set_integrable_Icc_isCont *)
-lemma set_integral_scaleR_right [simp]: "LINT t:A|M. a *\<^sub>R f t = a *\<^sub>R (LINT t:A|M. f t)"
+lemma set_integral_scaleR_right [simp]: "(LINT t:A|M. a *\<^sub>R f t) = a *\<^sub>R (LINT t:A|M. f t)"
unfolding set_lebesgue_integral_def
by (subst integral_scaleR_right[symmetric]) (auto intro!: Bochner_Integration.integral_cong)
lemma set_integral_mult_right [simp]:
fixes a :: "'a::{real_normed_field, second_countable_topology}"
- shows "LINT t:A|M. a * f t = a * (LINT t:A|M. f t)"
+ shows "(LINT t:A|M. a * f t) = a * (LINT t:A|M. f t)"
unfolding set_lebesgue_integral_def
by (subst integral_mult_right_zero[symmetric]) auto
lemma set_integral_mult_left [simp]:
fixes a :: "'a::{real_normed_field, second_countable_topology}"
- shows "LINT t:A|M. f t * a = (LINT t:A|M. f t) * a"
+ shows "(LINT t:A|M. f t * a) = (LINT t:A|M. f t) * a"
unfolding set_lebesgue_integral_def
by (subst integral_mult_left_zero[symmetric]) auto
lemma set_integral_divide_zero [simp]:
fixes a :: "'a::{real_normed_field, field, second_countable_topology}"
- shows "LINT t:A|M. f t / a = (LINT t:A|M. f t) / a"
+ shows "(LINT t:A|M. f t / a) = (LINT t:A|M. f t) / a"
unfolding set_lebesgue_integral_def
by (subst integral_divide_zero[symmetric], intro Bochner_Integration.integral_cong)
(auto split: split_indicator)
@@ -236,21 +236,20 @@
fixes f g :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
assumes "set_integrable M A f" "set_integrable M A g"
shows "set_integrable M A (\<lambda>x. f x + g x)"
- and "LINT x:A|M. f x + g x = (LINT x:A|M. f x) + (LINT x:A|M. g x)"
+ and "(LINT x:A|M. f x + g x) = (LINT x:A|M. f x) + (LINT x:A|M. g x)"
using assms unfolding set_integrable_def set_lebesgue_integral_def by (simp_all add: scaleR_add_right)
lemma set_integral_diff [simp, intro]:
assumes "set_integrable M A f" "set_integrable M A g"
- shows "set_integrable M A (\<lambda>x. f x - g x)" and "LINT x:A|M. f x - g x =
- (LINT x:A|M. f x) - (LINT x:A|M. g x)"
+ shows "set_integrable M A (\<lambda>x. f x - g x)" and "(LINT x:A|M. f x - g x) = (LINT x:A|M. f x) - (LINT x:A|M. g x)"
using assms unfolding set_integrable_def set_lebesgue_integral_def by (simp_all add: scaleR_diff_right)
-lemma set_integral_uminus: "set_integrable M A f \<Longrightarrow> LINT x:A|M. - f x = - (LINT x:A|M. f x)"
+lemma set_integral_uminus: "set_integrable M A f \<Longrightarrow> (LINT x:A|M. - f x) = - (LINT x:A|M. f x)"
unfolding set_integrable_def set_lebesgue_integral_def
by (subst integral_minus[symmetric]) simp_all
lemma set_integral_complex_of_real:
- "LINT x:A|M. complex_of_real (f x) = of_real (LINT x:A|M. f x)"
+ "(LINT x:A|M. complex_of_real (f x)) = of_real (LINT x:A|M. f x)"
unfolding set_lebesgue_integral_def
by (subst integral_complex_of_real[symmetric])
(auto intro!: Bochner_Integration.integral_cong split: split_indicator)
@@ -341,7 +340,7 @@
assumes "A \<inter> B = {}"
and "set_integrable M A f"
and "set_integrable M B f"
-shows "LINT x:A\<union>B|M. f x = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
+shows "(LINT x:A\<union>B|M. f x) = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
using assms
unfolding set_integrable_def set_lebesgue_integral_def
by (auto simp add: indicator_union_arith indicator_inter_arith[symmetric] scaleR_add_left)
@@ -350,7 +349,7 @@
fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
assumes "set_borel_measurable M A f" "set_borel_measurable M B f"
and ae: "AE x in M. x \<in> A \<longleftrightarrow> x \<in> B"
- shows "LINT x:B|M. f x = LINT x:A|M. f x"
+ shows "(LINT x:B|M. f x) = (LINT x:A|M. f x)"
unfolding set_lebesgue_integral_def
proof (rule integral_cong_AE)
show "AE x in M. indicator B x *\<^sub>R f x = indicator A x *\<^sub>R f x"
@@ -376,13 +375,13 @@
assumes ae: "AE x in M. \<not> (x \<in> A \<and> x \<in> B)" and [measurable]: "A \<in> sets M" "B \<in> sets M"
and "set_integrable M A f"
and "set_integrable M B f"
- shows "LINT x:A\<union>B|M. f x = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
+ shows "(LINT x:A\<union>B|M. f x) = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
proof -
have f: "set_integrable M (A \<union> B) f"
by (intro set_integrable_Un assms)
then have f': "set_borel_measurable M (A \<union> B) f"
using integrable_iff_bounded set_borel_measurable_def set_integrable_def by blast
- have "LINT x:A\<union>B|M. f x = LINT x:(A - A \<inter> B) \<union> (B - A \<inter> B)|M. f x"
+ have "(LINT x:A\<union>B|M. f x) = (LINT x:(A - A \<inter> B) \<union> (B - A \<inter> B)|M. f x)"
proof (rule set_integral_cong_set)
show "AE x in M. (x \<in> A - A \<inter> B \<union> (B - A \<inter> B)) = (x \<in> A \<union> B)"
using ae by auto
@@ -420,11 +419,11 @@
and intgbl: "\<And>i::nat. set_integrable M (A i) f"
and lim: "(\<lambda>i::nat. LINT x:A i|M. f x) \<longlonglongrightarrow> l"
shows "set_integrable M (\<Union>i. A i) f"
- unfolding set_integrable_def
+ unfolding set_integrable_def
apply (rule integrable_monotone_convergence[where f = "\<lambda>i::nat. \<lambda>x. indicator (A i) x *\<^sub>R f x" and x = l])
- apply (rule intgbl [unfolded set_integrable_def])
- prefer 3 apply (rule lim [unfolded set_lebesgue_integral_def])
- apply (rule AE_I2)
+ apply (rule intgbl [unfolded set_integrable_def])
+ prefer 3 apply (rule lim [unfolded set_lebesgue_integral_def])
+ apply (rule AE_I2)
using \<open>mono A\<close> apply (auto simp: mono_def nneg split: split_indicator) []
proof (rule AE_I2)
{ fix x assume "x \<in> space M"
@@ -432,18 +431,16 @@
proof cases
assume "\<exists>i. x \<in> A i"
then obtain i where "x \<in> A i" ..
- then have *: "eventually (\<lambda>i. x \<in> A i) sequentially"
+ then have "\<forall>\<^sub>F i in sequentially. x \<in> A i"
using \<open>x \<in> A i\<close> \<open>mono A\<close> by (auto simp: eventually_sequentially mono_def)
- show ?thesis
- apply (intro tendsto_eventually)
- using *
- apply eventually_elim
- apply (auto split: split_indicator)
- done
+ with eventually_mono have "\<forall>\<^sub>F i in sequentially. indicat_real (A i) x *\<^sub>R f x = indicat_real (\<Union> (range A)) x *\<^sub>R f x"
+ by fastforce
+ then show ?thesis
+ by (intro tendsto_eventually)
qed auto }
then show "(\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R f x) \<in> borel_measurable M"
apply (rule borel_measurable_LIMSEQ_real)
- apply assumption
+ apply assumption
using intgbl set_integrable_def by blast
qed
@@ -453,7 +450,7 @@
assumes meas[intro]: "\<And>i::nat. A i \<in> sets M"
and disj: "\<And>i j. i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
and intgbl: "set_integrable M (\<Union>i. A i) f"
- shows "LINT x:(\<Union>i. A i)|M. f x = (\<Sum>i. (LINT x:(A i)|M. f x))"
+ shows "(LINT x:(\<Union>i. A i)|M. f x) = (\<Sum>i. (LINT x:(A i)|M. f x))"
unfolding set_lebesgue_integral_def
proof (subst integral_suminf[symmetric])
show int_A: "integrable M (\<lambda>x. indicat_real (A i) x *\<^sub>R f x)" for i
@@ -503,7 +500,7 @@
fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
assumes [measurable]: "\<And>i. A i \<in> sets M" and A: "incseq A"
and intgbl: "set_integrable M (\<Union>i. A i) f"
-shows "(\<lambda>i. LINT x:(A i)|M. f x) \<longlonglongrightarrow> LINT x:(\<Union>i. A i)|M. f x"
+shows "(\<lambda>i. LINT x:(A i)|M. f x) \<longlonglongrightarrow> (LINT x:(\<Union>i. A i)|M. f x)"
unfolding set_lebesgue_integral_def
proof (intro integral_dominated_convergence[where w="\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R norm (f x)"])
have int_A: "\<And>i. set_integrable M (A i) f"
@@ -528,7 +525,7 @@
fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
assumes [measurable]: "\<And>i. A i \<in> sets M" and A: "decseq A"
and int0: "set_integrable M (A 0) f"
- shows "(\<lambda>i::nat. LINT x:(A i)|M. f x) \<longlonglongrightarrow> LINT x:(\<Inter>i. A i)|M. f x"
+ shows "(\<lambda>i::nat. LINT x:(A i)|M. f x) \<longlonglongrightarrow> (LINT x:(\<Inter>i. A i)|M. f x)"
unfolding set_lebesgue_integral_def
proof (rule integral_dominated_convergence)
have int_A: "\<And>i. set_integrable M (A i) f"
@@ -580,7 +577,7 @@
syntax
"_ascii_complex_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
- ("(3CLINT _|_. _)" [0,110,60] 60)
+ ("(3CLINT _|_. _)" [0,110,60] 10)
translations
"CLINT x|M. f" == "CONST complex_lebesgue_integral M (\<lambda>x. f)"
@@ -614,7 +611,7 @@
syntax
"_ascii_complex_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
-("(4CLINT _:_|_. _)" [0,60,110,61] 60)
+("(4CLINT _:_|_. _)" [0,60,110,61] 10)
translations
"CLINT x:A|M. f" == "CONST complex_set_lebesgue_integral M A (\<lambda>x. f)"
@@ -633,10 +630,10 @@
syntax
"_set_nn_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal"
-("(\<integral>\<^sup>+((_)\<in>(_)./ _)/\<partial>_)" [0,60,110,61] 60)
+("(\<integral>\<^sup>+((_)\<in>(_)./ _)/\<partial>_)" [0,60,110,61] 10)
"_set_lebesgue_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal"
-("(\<integral>((_)\<in>(_)./ _)/\<partial>_)" [0,60,110,61] 60)
+("(\<integral>((_)\<in>(_)./ _)/\<partial>_)" [0,60,110,61] 10)
translations
"\<integral>\<^sup>+x \<in> A. f \<partial>M" == "CONST set_nn_integral M A (\<lambda>x. f)"
--- a/src/HOL/Bit_Operations.thy Wed Feb 14 16:25:41 2024 +0100
+++ b/src/HOL/Bit_Operations.thy Thu Feb 15 08:25:25 2024 +0100
@@ -327,40 +327,6 @@
\<open>bit (a mod 2) n \<longleftrightarrow> n = 0 \<and> odd a\<close>
by (simp add: mod_2_eq_odd bit_simps)
-lemma bit_disjunctive_add_iff:
- \<open>bit (a + b) n \<longleftrightarrow> bit a n \<or> bit b n\<close>
- if \<open>\<And>n. \<not> bit a n \<or> \<not> bit b n\<close>
-proof (cases \<open>possible_bit TYPE('a) n\<close>)
- case False
- then show ?thesis
- by (auto dest: impossible_bit)
-next
- case True
- with that show ?thesis proof (induction n arbitrary: a b)
- case 0
- from "0.prems"(1) [of 0] show ?case
- by (auto simp add: bit_0)
- next
- case (Suc n)
- from Suc.prems(1) [of 0] have even: \<open>even a \<or> even b\<close>
- by (auto simp add: bit_0)
- have bit: \<open>\<not> bit (a div 2) n \<or> \<not> bit (b div 2) n\<close> for n
- using Suc.prems(1) [of \<open>Suc n\<close>] by (simp add: bit_Suc)
- from Suc.prems(2) have \<open>possible_bit TYPE('a) (Suc n)\<close> \<open>possible_bit TYPE('a) n\<close>
- by (simp_all add: possible_bit_less_imp)
- have \<open>a + b = (a div 2 * 2 + a mod 2) + (b div 2 * 2 + b mod 2)\<close>
- using div_mult_mod_eq [of a 2] div_mult_mod_eq [of b 2] by simp
- also have \<open>\<dots> = of_bool (odd a \<or> odd b) + 2 * (a div 2 + b div 2)\<close>
- using even by (auto simp add: algebra_simps mod2_eq_if)
- finally have \<open>bit ((a + b) div 2) n \<longleftrightarrow> bit (a div 2 + b div 2) n\<close>
- using \<open>possible_bit TYPE('a) (Suc n)\<close> by simp (simp_all flip: bit_Suc add: bit_double_iff possible_bit_def)
- also have \<open>\<dots> \<longleftrightarrow> bit (a div 2) n \<or> bit (b div 2) n\<close>
- using bit \<open>possible_bit TYPE('a) n\<close> by (rule Suc.IH)
- finally show ?case
- by (simp add: bit_Suc)
- qed
-qed
-
end
lemma nat_bit_induct [case_names zero even odd]:
@@ -723,10 +689,6 @@
\<open>even (a OR b) \<longleftrightarrow> even a \<and> even b\<close>
using bit_or_iff [of a b 0] by (auto simp add: bit_0)
-lemma disjunctive_add:
- \<open>a + b = a OR b\<close> if \<open>\<And>n. \<not> bit a n \<or> \<not> bit b n\<close>
- by (rule bit_eqI) (use that in \<open>simp add: bit_disjunctive_add_iff bit_or_iff\<close>)
-
lemma even_xor_iff:
\<open>even (a XOR b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)\<close>
using bit_xor_iff [of a b 0] by (auto simp add: bit_0)
@@ -1283,13 +1245,59 @@
\<open>take_bit n a = (\<Sum>k = 0..<n. push_bit k (of_bool (bit a k)))\<close>
by (simp flip: horner_sum_bit_eq_take_bit add: horner_sum_eq_sum push_bit_eq_mult)
+lemma disjunctive_xor_eq_or:
+ \<open>a XOR b = a OR b\<close> if \<open>a AND b = 0\<close>
+ using that by (auto simp add: bit_eq_iff bit_simps)
+
+lemma disjunctive_add_eq_or:
+ \<open>a + b = a OR b\<close> if \<open>a AND b = 0\<close>
+proof (rule bit_eqI)
+ fix n
+ assume \<open>possible_bit TYPE('a) n\<close>
+ moreover from that have \<open>\<And>n. \<not> bit (a AND b) n\<close>
+ by simp
+ then have \<open>\<And>n. \<not> bit a n \<or> \<not> bit b n\<close>
+ by (simp add: bit_simps)
+ ultimately show \<open>bit (a + b) n \<longleftrightarrow> bit (a OR b) n\<close>
+ proof (induction n arbitrary: a b)
+ case 0
+ from "0"(2)[of 0] show ?case
+ by (auto simp add: even_or_iff bit_0)
+ next
+ case (Suc n)
+ from Suc.prems(2) [of 0] have even: \<open>even a \<or> even b\<close>
+ by (auto simp add: bit_0)
+ have bit: \<open>\<not> bit (a div 2) n \<or> \<not> bit (b div 2) n\<close> for n
+ using Suc.prems(2) [of \<open>Suc n\<close>] by (simp add: bit_Suc)
+ from Suc.prems have \<open>possible_bit TYPE('a) n\<close>
+ using possible_bit_less_imp by force
+ with \<open>\<And>n. \<not> bit (a div 2) n \<or> \<not> bit (b div 2) n\<close> Suc.IH [of \<open>a div 2\<close> \<open>b div 2\<close>]
+ have IH: \<open>bit (a div 2 + b div 2) n \<longleftrightarrow> bit (a div 2 OR b div 2) n\<close>
+ by (simp add: bit_Suc)
+ have \<open>a + b = (a div 2 * 2 + a mod 2) + (b div 2 * 2 + b mod 2)\<close>
+ using div_mult_mod_eq [of a 2] div_mult_mod_eq [of b 2] by simp
+ also have \<open>\<dots> = of_bool (odd a \<or> odd b) + 2 * (a div 2 + b div 2)\<close>
+ using even by (auto simp add: algebra_simps mod2_eq_if)
+ finally have \<open>bit ((a + b) div 2) n \<longleftrightarrow> bit (a div 2 + b div 2) n\<close>
+ using \<open>possible_bit TYPE('a) (Suc n)\<close> by simp (simp_all flip: bit_Suc add: bit_double_iff possible_bit_def)
+ also have \<open>\<dots> \<longleftrightarrow> bit (a div 2 OR b div 2) n\<close>
+ by (rule IH)
+ finally show ?case
+ by (simp add: bit_simps flip: bit_Suc)
+ qed
+qed
+
+lemma disjunctive_add_eq_xor:
+ \<open>a + b = a XOR b\<close> if \<open>a AND b = 0\<close>
+ using that by (simp add: disjunctive_add_eq_or disjunctive_xor_eq_or)
+
lemma set_bit_eq:
\<open>set_bit n a = a + of_bool (\<not> bit a n) * 2 ^ n\<close>
proof -
- have \<open>set_bit n a = a OR of_bool (\<not> bit a n) * 2 ^ n\<close>
- by (rule bit_eqI) (auto simp add: bit_simps)
+ have \<open>a AND of_bool (\<not> bit a n) * 2 ^ n = 0\<close>
+ by (auto simp add: bit_eq_iff bit_simps)
then show ?thesis
- by (subst disjunctive_add) (auto simp add: bit_simps)
+ by (auto simp add: bit_eq_iff bit_simps disjunctive_add_eq_or)
qed
end
@@ -1417,17 +1425,25 @@
\<open>a AND b = - 1 \<longleftrightarrow> a = - 1 \<and> b = - 1\<close>
by (auto simp: bit_eq_iff bit_simps)
-lemma disjunctive_diff:
- \<open>a - b = a AND NOT b\<close> if \<open>\<And>n. bit b n \<Longrightarrow> bit a n\<close>
+lemma disjunctive_and_not_eq_xor:
+ \<open>a AND NOT b = a XOR b\<close> if \<open>NOT a AND b = 0\<close>
+ using that by (auto simp add: bit_eq_iff bit_simps)
+
+lemma disjunctive_diff_eq_and_not:
+ \<open>a - b = a AND NOT b\<close> if \<open>NOT a AND b = 0\<close>
proof -
- have \<open>NOT a + b = NOT a OR b\<close>
- by (rule disjunctive_add) (auto simp add: bit_not_iff dest: that)
+ from that have \<open>NOT a + b = NOT a OR b\<close>
+ by (rule disjunctive_add_eq_or)
then have \<open>NOT (NOT a + b) = NOT (NOT a OR b)\<close>
by simp
then show ?thesis
by (simp add: not_add_distrib)
qed
+lemma disjunctive_diff_eq_xor:
+ \<open>a AND NOT b = a XOR b\<close> if \<open>NOT a AND b = 0\<close>
+ using that by (simp add: disjunctive_and_not_eq_xor disjunctive_diff_eq_and_not)
+
lemma push_bit_minus:
\<open>push_bit n (- a) = - push_bit n a\<close>
by (simp add: push_bit_eq_mult)
@@ -1443,15 +1459,12 @@
lemma take_bit_not_eq_mask_diff:
\<open>take_bit n (NOT a) = mask n - take_bit n a\<close>
proof -
- have \<open>take_bit n (NOT a) = take_bit n (NOT (take_bit n a))\<close>
- by (simp add: take_bit_not_take_bit)
- also have \<open>\<dots> = mask n AND NOT (take_bit n a)\<close>
- by (simp add: take_bit_eq_mask ac_simps)
- also have \<open>\<dots> = mask n - take_bit n a\<close>
- by (subst disjunctive_diff)
- (auto simp add: bit_take_bit_iff bit_mask_iff bit_imp_possible_bit)
- finally show ?thesis
- by simp
+ have \<open>NOT (mask n) AND take_bit n a = 0\<close>
+ by (simp add: bit_eq_iff bit_simps)
+ moreover have \<open>take_bit n (NOT a) = mask n AND NOT (take_bit n a)\<close>
+ by (auto simp add: bit_eq_iff bit_simps)
+ ultimately show ?thesis
+ by (simp add: disjunctive_diff_eq_and_not)
qed
lemma mask_eq_take_bit_minus_one:
@@ -1512,10 +1525,12 @@
lemma unset_bit_eq:
\<open>unset_bit n a = a - of_bool (bit a n) * 2 ^ n\<close>
proof -
- have \<open>unset_bit n a = a AND NOT (of_bool (bit a n) * 2 ^ n)\<close>
- by (rule bit_eqI) (auto simp add: bit_simps)
- then show ?thesis
- by (subst disjunctive_diff) (auto simp add: bit_simps simp flip: push_bit_eq_mult)
+ have \<open>NOT a AND of_bool (bit a n) * 2 ^ n = 0\<close>
+ by (auto simp add: bit_eq_iff bit_simps)
+ moreover have \<open>unset_bit n a = a AND NOT (of_bool (bit a n) * 2 ^ n)\<close>
+ by (auto simp add: bit_eq_iff bit_simps)
+ ultimately show ?thesis
+ by (simp add: disjunctive_diff_eq_and_not)
qed
end
@@ -3327,8 +3342,12 @@
lemma concat_bit_eq:
\<open>concat_bit n k l = take_bit n k + push_bit n l\<close>
- by (simp add: concat_bit_def take_bit_eq_mask
- bit_and_iff bit_mask_iff bit_push_bit_iff disjunctive_add)
+proof -
+ have \<open>take_bit n k AND push_bit n l = 0\<close>
+ by (simp add: bit_eq_iff bit_simps)
+ then show ?thesis
+ by (simp add: bit_eq_iff bit_simps disjunctive_add_eq_or)
+qed
lemma concat_bit_0 [simp]:
\<open>concat_bit 0 k l = l\<close>
@@ -3479,6 +3498,26 @@
using that by (rule le_SucE; intro bit_eqI)
(auto simp add: bit_take_bit_iff bit_signed_take_bit_iff min_def less_Suc_eq)
+lemma signed_take_bit_eq_take_bit_add:
+ \<open>signed_take_bit n k = take_bit (Suc n) k + NOT (mask (Suc n)) * of_bool (bit k n)\<close>
+proof (cases \<open>bit k n\<close>)
+ case False
+ show ?thesis
+ by (rule bit_eqI) (simp add: False bit_simps min_def less_Suc_eq)
+next
+ case True
+ have \<open>signed_take_bit n k = take_bit (Suc n) k OR NOT (mask (Suc n))\<close>
+ by (rule bit_eqI) (auto simp add: bit_signed_take_bit_iff min_def bit_take_bit_iff bit_or_iff bit_not_iff bit_mask_iff less_Suc_eq True)
+ also have \<open>\<dots> = take_bit (Suc n) k + NOT (mask (Suc n))\<close>
+ by (simp add: disjunctive_add_eq_or bit_eq_iff bit_simps)
+ finally show ?thesis
+ by (simp add: True)
+qed
+
+lemma signed_take_bit_eq_take_bit_minus:
+ \<open>signed_take_bit n k = take_bit (Suc n) k - 2 ^ Suc n * of_bool (bit k n)\<close>
+ by (simp add: signed_take_bit_eq_take_bit_add flip: minus_exp_eq_not_mask)
+
end
text \<open>Modulus centered around 0\<close>
@@ -3538,34 +3577,18 @@
by (simp only: signed_take_bit_eq_iff_take_bit_eq take_bit_mult)
qed
-lemma signed_take_bit_eq_take_bit_minus:
- \<open>signed_take_bit n k = take_bit (Suc n) k - 2 ^ Suc n * of_bool (bit k n)\<close>
- for k :: int
-proof (cases \<open>bit k n\<close>)
- case True
- have \<open>signed_take_bit n k = take_bit (Suc n) k OR NOT (mask (Suc n))\<close>
- by (rule bit_eqI) (auto simp add: bit_signed_take_bit_iff min_def bit_take_bit_iff bit_or_iff bit_not_iff bit_mask_iff less_Suc_eq True)
- then have \<open>signed_take_bit n k = take_bit (Suc n) k + NOT (mask (Suc n))\<close>
- by (simp add: disjunctive_add bit_take_bit_iff bit_not_iff bit_mask_iff)
- with True show ?thesis
- by (simp flip: minus_exp_eq_not_mask)
-next
- case False
- show ?thesis
- by (rule bit_eqI) (simp add: False bit_signed_take_bit_iff bit_take_bit_iff min_def less_Suc_eq)
-qed
-
lemma signed_take_bit_eq_take_bit_shift:
- \<open>signed_take_bit n k = take_bit (Suc n) (k + 2 ^ n) - 2 ^ n\<close>
+ \<open>signed_take_bit n k = take_bit (Suc n) (k + 2 ^ n) - 2 ^ n\<close> (is \<open>?lhs = ?rhs\<close>)
for k :: int
proof -
- have *: \<open>take_bit n k OR 2 ^ n = take_bit n k + 2 ^ n\<close>
- by (simp add: disjunctive_add bit_exp_iff bit_take_bit_iff)
+ have \<open>take_bit n k AND 2 ^ n = 0\<close>
+ by (rule bit_eqI) (simp add: bit_simps)
+ then have *: \<open>take_bit n k OR 2 ^ n = take_bit n k + 2 ^ n\<close>
+ by (simp add: disjunctive_add_eq_or)
have \<open>take_bit n k - 2 ^ n = take_bit n k + NOT (mask n)\<close>
by (simp add: minus_exp_eq_not_mask)
also have \<open>\<dots> = take_bit n k OR NOT (mask n)\<close>
- by (rule disjunctive_add)
- (simp add: bit_exp_iff bit_take_bit_iff bit_not_iff bit_mask_iff)
+ by (rule disjunctive_add_eq_or) (simp add: bit_eq_iff bit_simps)
finally have **: \<open>take_bit n k - 2 ^ n = take_bit n k OR NOT (mask n)\<close> .
have \<open>take_bit (Suc n) (k + 2 ^ n) = take_bit (Suc n) (take_bit (Suc n) k + take_bit (Suc n) (2 ^ n))\<close>
by (simp only: take_bit_add)
@@ -3574,8 +3597,7 @@
finally have \<open>take_bit (Suc n) (k + 2 ^ n) = take_bit (Suc n) (2 ^ (n + of_bool (bit k n)) + take_bit n k)\<close>
by (simp add: ac_simps)
also have \<open>2 ^ (n + of_bool (bit k n)) + take_bit n k = 2 ^ (n + of_bool (bit k n)) OR take_bit n k\<close>
- by (rule disjunctive_add)
- (auto simp add: disjunctive_add bit_take_bit_iff bit_double_iff bit_exp_iff)
+ by (rule disjunctive_add_eq_or, rule bit_eqI) (simp add: bit_simps)
finally show ?thesis
using * ** by (simp add: signed_take_bit_def concat_bit_Suc min_def ac_simps)
qed
@@ -3681,16 +3703,7 @@
\<open>signed_take_bit n a =
(let l = take_bit (Suc n) a
in if bit l n then l + push_bit (Suc n) (- 1) else l)\<close>
-proof -
- have *: \<open>take_bit (Suc n) a + push_bit n (- 2) =
- take_bit (Suc n) a OR NOT (mask (Suc n))\<close>
- by (auto simp add: bit_take_bit_iff bit_push_bit_iff bit_not_iff bit_mask_iff disjunctive_add
- simp flip: push_bit_minus_one_eq_not_mask)
- show ?thesis
- by (rule bit_eqI)
- (auto simp add: Let_def * bit_signed_take_bit_iff bit_take_bit_iff min_def less_Suc_eq bit_not_iff
- bit_mask_iff bit_or_iff simp del: push_bit_minus_one_eq_not_mask)
-qed
+ by (simp add: signed_take_bit_eq_take_bit_add bit_simps)
subsection \<open>Key ideas of bit operations\<close>
@@ -3833,6 +3846,40 @@
\<open>\<not> bit a n\<close> if \<open>2 ^ n = 0\<close>
using that by (simp add: bit_iff_odd)
+lemma bit_disjunctive_add_iff [no_atp]:
+ \<open>bit (a + b) n \<longleftrightarrow> bit a n \<or> bit b n\<close>
+ if \<open>\<And>n. \<not> bit a n \<or> \<not> bit b n\<close>
+proof (cases \<open>possible_bit TYPE('a) n\<close>)
+ case False
+ then show ?thesis
+ by (auto dest: impossible_bit)
+next
+ case True
+ with that show ?thesis proof (induction n arbitrary: a b)
+ case 0
+ from "0.prems"(1) [of 0] show ?case
+ by (auto simp add: bit_0)
+ next
+ case (Suc n)
+ from Suc.prems(1) [of 0] have even: \<open>even a \<or> even b\<close>
+ by (auto simp add: bit_0)
+ have bit: \<open>\<not> bit (a div 2) n \<or> \<not> bit (b div 2) n\<close> for n
+ using Suc.prems(1) [of \<open>Suc n\<close>] by (simp add: bit_Suc)
+ from Suc.prems(2) have \<open>possible_bit TYPE('a) (Suc n)\<close> \<open>possible_bit TYPE('a) n\<close>
+ by (simp_all add: possible_bit_less_imp)
+ have \<open>a + b = (a div 2 * 2 + a mod 2) + (b div 2 * 2 + b mod 2)\<close>
+ using div_mult_mod_eq [of a 2] div_mult_mod_eq [of b 2] by simp
+ also have \<open>\<dots> = of_bool (odd a \<or> odd b) + 2 * (a div 2 + b div 2)\<close>
+ using even by (auto simp add: algebra_simps mod2_eq_if)
+ finally have \<open>bit ((a + b) div 2) n \<longleftrightarrow> bit (a div 2 + b div 2) n\<close>
+ using \<open>possible_bit TYPE('a) (Suc n)\<close> by simp (simp_all flip: bit_Suc add: bit_double_iff possible_bit_def)
+ also have \<open>\<dots> \<longleftrightarrow> bit (a div 2) n \<or> bit (b div 2) n\<close>
+ using bit \<open>possible_bit TYPE('a) n\<close> by (rule Suc.IH)
+ finally show ?case
+ by (simp add: bit_Suc)
+ qed
+qed
+
end
context semiring_bit_operations
@@ -3870,6 +3917,26 @@
lemmas flip_bit_def [no_atp] = flip_bit_eq_xor
+lemma disjunctive_add [no_atp]:
+ \<open>a + b = a OR b\<close> if \<open>\<And>n. \<not> bit a n \<or> \<not> bit b n\<close>
+ by (rule disjunctive_add_eq_or) (use that in \<open>simp add: bit_eq_iff bit_simps\<close>)
+
+end
+
+context ring_bit_operations
+begin
+
+lemma disjunctive_diff [no_atp]:
+ \<open>a - b = a AND NOT b\<close> if \<open>\<And>n. bit b n \<Longrightarrow> bit a n\<close>
+proof -
+ have \<open>NOT a + b = NOT a OR b\<close>
+ by (rule disjunctive_add) (auto simp add: bit_not_iff dest: that)
+ then have \<open>NOT (NOT a + b) = NOT (NOT a OR b)\<close>
+ by simp
+ then show ?thesis
+ by (simp add: not_add_distrib)
+qed
+
end
lemma and_nat_rec [no_atp]:
--- a/src/HOL/Fun.thy Wed Feb 14 16:25:41 2024 +0100
+++ b/src/HOL/Fun.thy Thu Feb 15 08:25:25 2024 +0100
@@ -395,6 +395,11 @@
lemma bij_betw_comp_iff: "bij_betw f A A' \<Longrightarrow> bij_betw f' A' A'' \<longleftrightarrow> bij_betw (f' \<circ> f) A A''"
by (auto simp add: bij_betw_def inj_on_def)
+lemma bij_betw_Collect:
+ assumes "bij_betw f A B" "\<And>x. x \<in> A \<Longrightarrow> Q (f x) \<longleftrightarrow> P x"
+ shows "bij_betw f {x\<in>A. P x} {y\<in>B. Q y}"
+ using assms by (auto simp add: bij_betw_def inj_on_def)
+
lemma bij_betw_comp_iff2:
assumes bij: "bij_betw f' A' A''"
and img: "f ` A \<le> A'"
--- a/src/HOL/Fun_Def.thy Wed Feb 14 16:25:41 2024 +0100
+++ b/src/HOL/Fun_Def.thy Thu Feb 15 08:25:25 2024 +0100
@@ -304,7 +304,7 @@
done
-subsection \<open>Yet another induction principle on the natural numbers\<close>
+subsection \<open>Yet more induction principles on the natural numbers\<close>
lemma nat_descend_induct [case_names base descend]:
fixes P :: "nat \<Rightarrow> bool"
@@ -313,6 +313,13 @@
shows "P m"
using assms by induction_schema (force intro!: wf_measure [of "\<lambda>k. Suc n - k"])+
+lemma induct_nat_012[case_names 0 1 ge2]:
+ "P 0 \<Longrightarrow> P (Suc 0) \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (Suc n) \<Longrightarrow> P (Suc (Suc n))) \<Longrightarrow> P n"
+proof (induction_schema, pat_completeness)
+ show "wf (Wellfounded.measure id)"
+ by simp
+qed auto
+
subsection \<open>Tool setup\<close>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Infinite_Typeclass.thy Thu Feb 15 08:25:25 2024 +0100
@@ -0,0 +1,47 @@
+(* Title: HOL/Library/Infinite_Typeclass.thy
+*)
+
+section \<open>Infinite Type Class\<close>
+text \<open>The type class of infinite sets (orginally from the Incredible Proof Machine)\<close>
+
+theory Infinite_Typeclass
+ imports Complex_Main
+begin
+
+class infinite =
+ assumes infinite_UNIV: "infinite (UNIV::'a set)"
+
+instance nat :: infinite
+ by (intro_classes) simp
+
+instance int :: infinite
+ by (intro_classes) simp
+
+instance rat :: infinite
+proof
+ show "infinite (UNIV::rat set)"
+ by (simp add: infinite_UNIV_char_0)
+qed
+
+instance real :: infinite
+proof
+ show "infinite (UNIV::real set)"
+ by (simp add: infinite_UNIV_char_0)
+qed
+
+instance complex :: infinite
+proof
+ show "infinite (UNIV::complex set)"
+ by (simp add: infinite_UNIV_char_0)
+qed
+
+instance option :: (infinite) infinite
+ by intro_classes (simp add: infinite_UNIV)
+
+instance prod :: (infinite, type) infinite
+ by intro_classes (simp add: finite_prod infinite_UNIV)
+
+instance list :: (type) infinite
+ by intro_classes (simp add: infinite_UNIV_listI)
+
+end
--- a/src/HOL/Library/Library.thy Wed Feb 14 16:25:41 2024 +0100
+++ b/src/HOL/Library/Library.thy Thu Feb 15 08:25:25 2024 +0100
@@ -41,6 +41,7 @@
Groups_Big_Fun
Indicator_Function
Infinite_Set
+ Infinite_Typeclass
Interval
Interval_Float
IArray
--- a/src/HOL/List.thy Wed Feb 14 16:25:41 2024 +0100
+++ b/src/HOL/List.thy Thu Feb 15 08:25:25 2024 +0100
@@ -4118,6 +4118,21 @@
successively P (remdups_adj xs) \<longleftrightarrow> successively P xs"
by (induction xs rule: remdups_adj.induct)(auto simp: successively_Cons)
+lemma successively_conv_nth:
+ "successively P xs \<longleftrightarrow> (\<forall>i. Suc i < length xs \<longrightarrow> P (xs ! i) (xs ! Suc i))"
+ by (induction P xs rule: successively.induct)
+ (force simp: nth_Cons split: nat.splits)+
+
+lemma successively_nth: "successively P xs \<Longrightarrow> Suc i < length xs \<Longrightarrow> P (xs ! i) (xs ! Suc i)"
+ unfolding successively_conv_nth by blast
+
+lemma distinct_adj_conv_nth:
+ "distinct_adj xs \<longleftrightarrow> (\<forall>i. Suc i < length xs \<longrightarrow> xs ! i \<noteq> xs ! Suc i)"
+ by (simp add: distinct_adj_def successively_conv_nth)
+
+lemma distinct_adj_nth: "distinct_adj xs \<Longrightarrow> Suc i < length xs \<Longrightarrow> xs ! i \<noteq> xs ! Suc i"
+ unfolding distinct_adj_conv_nth by blast
+
lemma remdups_adj_Cons':
"remdups_adj (x # xs) = x # remdups_adj (dropWhile (\<lambda>y. y = x) xs)"
by (induction xs) auto
@@ -4163,6 +4178,34 @@
\<Longrightarrow> remdups_adj (xs @ ys) = remdups_adj xs @ remdups_adj (dropWhile (\<lambda>y. y = last xs) ys)"
by (induction xs rule: remdups_adj.induct) (auto simp: remdups_adj_Cons')
+lemma remdups_filter_last:
+ "last [x\<leftarrow>remdups xs. P x] = last [x\<leftarrow>xs. P x]"
+by (induction xs, auto simp: filter_empty_conv)
+
+lemma remdups_append:
+ "set xs \<subseteq> set ys \<Longrightarrow> remdups (xs @ ys) = remdups ys"
+ by (induction xs, simp_all)
+
+lemma remdups_concat:
+ "remdups (concat (remdups xs)) = remdups (concat xs)"
+proof (induction xs)
+ case Nil
+ then show ?case by simp
+next
+ case (Cons a xs)
+ show ?case
+ proof (cases "a \<in> set xs")
+ case True
+ then have "remdups (concat xs) = remdups (a @ concat xs)"
+ by (metis remdups_append concat.simps(2) insert_absorb set_simps(2) set_append set_concat sup_ge1)
+ then show ?thesis
+ by (simp add: Cons True)
+ next
+ case False
+ then show ?thesis
+ by (metis Cons remdups_append2 concat.simps(2) remdups.simps(2))
+ qed
+qed
subsection \<open>@{const distinct_adj}\<close>
@@ -4213,6 +4256,14 @@
lemma distinct_adj_map_iff: "inj_on f (set xs) \<Longrightarrow> distinct_adj (map f xs) \<longleftrightarrow> distinct_adj xs"
using distinct_adj_mapD distinct_adj_mapI by blast
+lemma distinct_adj_conv_length_remdups_adj:
+ "distinct_adj xs \<longleftrightarrow> length (remdups_adj xs) = length xs"
+proof (induction xs rule: remdups_adj.induct)
+ case (3 x y xs)
+ thus ?case
+ using remdups_adj_length[of "y # xs"] by auto
+qed auto
+
subsubsection \<open>\<^const>\<open>insert\<close>\<close>
@@ -4379,33 +4430,32 @@
lemma length_remove1:
"length(remove1 x xs) = (if x \<in> set xs then length xs - 1 else length xs)"
-by (induct xs) (auto dest!:length_pos_if_in_set)
+ by (induct xs) (auto dest!:length_pos_if_in_set)
lemma remove1_filter_not[simp]:
"\<not> P x \<Longrightarrow> remove1 x (filter P xs) = filter P xs"
-by(induct xs) auto
+ by(induct xs) auto
lemma filter_remove1:
"filter Q (remove1 x xs) = remove1 x (filter Q xs)"
-by (induct xs) auto
+ by (induct xs) auto
lemma notin_set_remove1[simp]: "x \<notin> set xs \<Longrightarrow> x \<notin> set(remove1 y xs)"
-by(insert set_remove1_subset) fast
+ by(insert set_remove1_subset) fast
lemma distinct_remove1[simp]: "distinct xs \<Longrightarrow> distinct(remove1 x xs)"
-by (induct xs) simp_all
+ by (induct xs) simp_all
lemma remove1_remdups:
"distinct xs \<Longrightarrow> remove1 x (remdups xs) = remdups (remove1 x xs)"
-by (induct xs) simp_all
+ by (induct xs) simp_all
lemma remove1_idem: "x \<notin> set xs \<Longrightarrow> remove1 x xs = xs"
-by (induct xs) simp_all
+ by (induct xs) simp_all
lemma remove1_split:
"a \<in> set xs \<Longrightarrow> remove1 a xs = ys \<longleftrightarrow> (\<exists>ls rs. xs = ls @ a # rs \<and> a \<notin> set ls \<and> ys = ls @ rs)"
-by (metis remove1.simps(2) remove1_append split_list_first)
-
+ by (metis remove1.simps(2) remove1_append split_list_first)
subsubsection \<open>\<^const>\<open>removeAll\<close>\<close>
--- a/src/HOL/Probability/Characteristic_Functions.thy Wed Feb 14 16:25:41 2024 +0100
+++ b/src/HOL/Probability/Characteristic_Functions.thy Thu Feb 15 08:25:25 2024 +0100
@@ -56,8 +56,7 @@
definition
char :: "real measure \<Rightarrow> real \<Rightarrow> complex"
-where
- "char M t = CLINT x|M. iexp (t * x)"
+ where "char M t \<equiv> CLINT x|M. iexp (t * x)"
lemma (in real_distribution) char_zero: "char M 0 = 1"
unfolding char_def by (simp del: space_eq_univ add: prob_space)
--- a/src/HOL/Probability/Conditional_Expectation.thy Wed Feb 14 16:25:41 2024 +0100
+++ b/src/HOL/Probability/Conditional_Expectation.thy Thu Feb 15 08:25:25 2024 +0100
@@ -355,13 +355,13 @@
fix A assume "A \<in> sets F"
then have [measurable]: "(\<lambda>x. f x * indicator A x) \<in> borel_measurable F" by measurable
- have "\<integral>\<^sup>+x\<in>A. (f x * g x) \<partial>M = \<integral>\<^sup>+x. (f x * indicator A x) * g x \<partial>M"
+ have "(\<integral>\<^sup>+x\<in>A. (f x * g x) \<partial>M) = \<integral>\<^sup>+x. (f x * indicator A x) * g x \<partial>M"
by (simp add: mult.commute mult.left_commute)
also have "... = \<integral>\<^sup>+x. (f x * indicator A x) * nn_cond_exp M F g x \<partial>M"
by (rule nn_cond_exp_intg[symmetric]) (auto simp add: assms)
- also have "... = \<integral>\<^sup>+x\<in>A. (f x * nn_cond_exp M F g x)\<partial>M"
+ also have "... = (\<integral>\<^sup>+x\<in>A. (f x * nn_cond_exp M F g x)\<partial>M)"
by (simp add: mult.commute mult.left_commute)
- finally show "\<integral>\<^sup>+x\<in>A. (f x * g x) \<partial>M = \<integral>\<^sup>+x\<in>A. (f x * nn_cond_exp M F g x)\<partial>M" by simp
+ finally show "(\<integral>\<^sup>+x\<in>A. (f x * g x) \<partial>M) = (\<integral>\<^sup>+x\<in>A. (f x * nn_cond_exp M F g x)\<partial>M)" by simp
qed (auto simp add: assms)
lemma nn_cond_exp_sum:
@@ -370,7 +370,7 @@
proof (rule nn_cond_exp_charact)
fix A assume [measurable]: "A \<in> sets F"
then have "A \<in> sets M" by (meson subalg subalgebra_def subsetD)
- have "\<integral>\<^sup>+x\<in>A. (nn_cond_exp M F f x + nn_cond_exp M F g x)\<partial>M = (\<integral>\<^sup>+x\<in>A. nn_cond_exp M F f x \<partial>M) + (\<integral>\<^sup>+x\<in>A. nn_cond_exp M F g x \<partial>M)"
+ have "(\<integral>\<^sup>+x\<in>A. (nn_cond_exp M F f x + nn_cond_exp M F g x)\<partial>M) = (\<integral>\<^sup>+x\<in>A. nn_cond_exp M F f x \<partial>M) + (\<integral>\<^sup>+x\<in>A. nn_cond_exp M F g x \<partial>M)"
by (rule nn_set_integral_add) (auto simp add: assms \<open>A \<in> sets M\<close>)
also have "... = (\<integral>\<^sup>+x. indicator A x * nn_cond_exp M F f x \<partial>M) + (\<integral>\<^sup>+x. indicator A x * nn_cond_exp M F g x \<partial>M)"
by (metis (no_types, lifting) mult.commute nn_integral_cong)
@@ -378,9 +378,9 @@
by (simp add: nn_cond_exp_intg)
also have "... = (\<integral>\<^sup>+x\<in>A. f x \<partial>M) + (\<integral>\<^sup>+x\<in>A. g x \<partial>M)"
by (metis (no_types, lifting) mult.commute nn_integral_cong)
- also have "... = \<integral>\<^sup>+x\<in>A. (f x + g x)\<partial>M"
+ also have "... = (\<integral>\<^sup>+x\<in>A. (f x + g x)\<partial>M)"
by (rule nn_set_integral_add[symmetric]) (auto simp add: assms \<open>A \<in> sets M\<close>)
- finally show "\<integral>\<^sup>+x\<in>A. (f x + g x)\<partial>M = \<integral>\<^sup>+x\<in>A. (nn_cond_exp M F f x + nn_cond_exp M F g x)\<partial>M"
+ finally show "(\<integral>\<^sup>+x\<in>A. (f x + g x)\<partial>M) = (\<integral>\<^sup>+x\<in>A. (nn_cond_exp M F f x + nn_cond_exp M F g x)\<partial>M)"
by simp
qed (auto simp add: assms)
@@ -390,12 +390,12 @@
shows "AE x in M. nn_cond_exp M F f x = nn_cond_exp M F g x"
proof (rule nn_cond_exp_charact)
fix A assume [measurable]: "A \<in> sets F"
- have "\<integral>\<^sup>+x\<in>A. nn_cond_exp M F f x \<partial>M = \<integral>\<^sup>+x. indicator A x * nn_cond_exp M F f x \<partial>M"
+ have "(\<integral>\<^sup>+x\<in>A. nn_cond_exp M F f x \<partial>M) = \<integral>\<^sup>+x. indicator A x * nn_cond_exp M F f x \<partial>M"
by (simp add: mult.commute)
also have "... = \<integral>\<^sup>+x. indicator A x * f x \<partial>M" by (simp add: nn_cond_exp_intg assms)
- also have "... = \<integral>\<^sup>+x\<in>A. f x \<partial>M" by (simp add: mult.commute)
- also have "... = \<integral>\<^sup>+x\<in>A. g x \<partial>M" by (rule nn_set_integral_cong[OF assms(1)])
- finally show "\<integral>\<^sup>+x\<in>A. g x \<partial>M = \<integral>\<^sup>+x\<in>A. nn_cond_exp M F f x \<partial>M" by simp
+ also have "... = (\<integral>\<^sup>+x\<in>A. f x \<partial>M)" by (simp add: mult.commute)
+ also have "... = (\<integral>\<^sup>+x\<in>A. g x \<partial>M)" by (rule nn_set_integral_cong[OF assms(1)])
+ finally show "(\<integral>\<^sup>+x\<in>A. g x \<partial>M) = (\<integral>\<^sup>+x\<in>A. nn_cond_exp M F f x \<partial>M)" by simp
qed (auto simp add: assms)
lemma nn_cond_exp_mono:
@@ -791,14 +791,14 @@
fix A assume "A \<in> sets F"
then have [measurable]: "(\<lambda>x. f x * indicator A x) \<in> borel_measurable F" by measurable
have [measurable]: "A \<in> sets M" using subalg by (meson \<open>A \<in> sets F\<close> subalgebra_def subsetD)
- have "\<integral>x\<in>A. (f x * g x) \<partial>M = \<integral>x. (f x * indicator A x) * g x \<partial>M"
+ have "(\<integral>x\<in>A. (f x * g x) \<partial>M) = \<integral>x. (f x * indicator A x) * g x \<partial>M"
by (simp add: mult.commute mult.left_commute set_lebesgue_integral_def)
also have "... = \<integral>x. (f x * indicator A x) * real_cond_exp M F g x \<partial>M"
apply (rule real_cond_exp_intg(2)[symmetric], auto simp add: assms)
using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(3)] by (simp add: mult.commute mult.left_commute)
- also have "... = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M"
+ also have "... = (\<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M)"
by (simp add: mult.commute mult.left_commute set_lebesgue_integral_def)
- finally show "\<integral>x\<in>A. (f x * g x) \<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M" by simp
+ finally show "(\<integral>x\<in>A. (f x * g x) \<partial>M) = (\<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M)" by simp
qed (auto simp add: real_cond_exp_intg(1) assms)
lemma real_cond_exp_add [intro]:
@@ -817,7 +817,7 @@
have intAg: "integrable M (\<lambda>x. indicator A x * g x)"
using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(2)] by auto
- have "\<integral>x\<in>A. (real_cond_exp M F f x + real_cond_exp M F g x)\<partial>M = (\<integral>x\<in>A. real_cond_exp M F f x \<partial>M) + (\<integral>x\<in>A. real_cond_exp M F g x \<partial>M)"
+ have "(\<integral>x\<in>A. (real_cond_exp M F f x + real_cond_exp M F g x)\<partial>M) = (\<integral>x\<in>A. real_cond_exp M F f x \<partial>M) + (\<integral>x\<in>A. real_cond_exp M F g x \<partial>M)"
apply (rule set_integral_add, auto simp add: assms set_integrable_def)
using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> real_cond_exp_int(1)[OF assms(1)]]
integrable_mult_indicator[OF \<open>A \<in> sets M\<close> real_cond_exp_int(1)[OF assms(2)]] by simp_all
@@ -827,9 +827,9 @@
using real_cond_exp_intg(2) assms \<open>A \<in> sets F\<close> intAf intAg by auto
also have "... = (\<integral>x\<in>A. f x \<partial>M) + (\<integral>x\<in>A. g x \<partial>M)"
unfolding set_lebesgue_integral_def by auto
- also have "... = \<integral>x\<in>A. (f x + g x)\<partial>M"
+ also have "... = (\<integral>x\<in>A. (f x + g x)\<partial>M)"
by (rule set_integral_add(2)[symmetric]) (auto simp add: assms set_integrable_def \<open>A \<in> sets M\<close> intAf intAg)
- finally show "\<integral>x\<in>A. (f x + g x)\<partial>M = \<integral>x\<in>A. (real_cond_exp M F f x + real_cond_exp M F g x)\<partial>M"
+ finally show "(\<integral>x\<in>A. (f x + g x)\<partial>M) = (\<integral>x\<in>A. (real_cond_exp M F f x + real_cond_exp M F g x)\<partial>M)"
by simp
qed (auto simp add: assms)
--- a/src/HOL/Probability/Levy.thy Wed Feb 14 16:25:41 2024 +0100
+++ b/src/HOL/Probability/Levy.thy Thu Feb 15 08:25:25 2024 +0100
@@ -375,10 +375,10 @@
have 3: "\<And>u v. integrable lborel (\<lambda>x. indicat_real {u..v} x *\<^sub>R cmod (1 - char M' x))"
by (intro borel_integrable_compact[OF compact_Icc] continuous_at_imp_continuous_on
continuous_intros ballI M'.isCont_char continuous_intros)
- have "cmod (CLBINT t:{-d/2..d/2}. 1 - char M' t) \<le> LBINT t:{-d/2..d/2}. cmod (1 - char M' t)"
+ have "cmod (CLBINT t:{-d/2..d/2}. 1 - char M' t) \<le> (LBINT t:{-d/2..d/2}. cmod (1 - char M' t))"
unfolding set_lebesgue_integral_def
using integral_norm_bound[of _ "\<lambda>x. indicator {u..v} x *\<^sub>R (1 - char M' x)" for u v] by simp
- also have 4: "\<dots> \<le> LBINT t:{-d/2..d/2}. \<epsilon> / 4"
+ also have 4: "\<dots> \<le> (LBINT t:{-d/2..d/2}. \<epsilon> / 4)"
unfolding set_lebesgue_integral_def
proof (rule integral_mono [OF 3])
--- a/src/HOL/Probability/Sinc_Integral.thy Wed Feb 14 16:25:41 2024 +0100
+++ b/src/HOL/Probability/Sinc_Integral.thy Thu Feb 15 08:25:25 2024 +0100
@@ -216,7 +216,7 @@
using has_bochner_integral_I0i_power_exp_m[of 0] has_bochner_integral_I0i_power_exp_m[of 1]
by (intro set_integral_add) (auto dest!: integrable.intros simp: ac_simps set_integrable_def)
- have "((\<lambda>t::real. LBINT x:{0<..}. ?F x t) \<longlongrightarrow> LBINT x::real:{0<..}. 0) at_top"
+ have "((\<lambda>t::real. LBINT x:{0<..}. ?F x t) \<longlongrightarrow> (LBINT x::real:{0<..}. 0)) at_top"
unfolding set_lebesgue_integral_def
proof (rule integral_dominated_convergence_at_top[OF _ _ int [unfolded set_integrable_def]],
simp_all del: abs_divide split: split_indicator)
@@ -278,23 +278,23 @@
have "Si t = LBINT x=0..t. sin x * (LBINT u=0..\<infinity>. exp (-(u * x)))"
unfolding Si_def using \<open>0 \<le> t\<close>
by (intro interval_integral_discrete_difference[where X="{0}"]) (auto simp: LBINT_I0i_exp_mscale)
- also have "\<dots> = LBINT x. (LBINT u=ereal 0..\<infinity>. indicator {0 <..< t} x *\<^sub>R sin x * exp (-(u * x)))"
+ also have "\<dots> = (LBINT x. (LBINT u=ereal 0..\<infinity>. indicator {0 <..< t} x *\<^sub>R sin x * exp (-(u * x))))"
using \<open>0\<le>t\<close> by (simp add: zero_ereal_def interval_lebesgue_integral_le_eq mult_ac set_lebesgue_integral_def)
- also have "\<dots> = LBINT x. (LBINT u. indicator ({0<..} \<times> {0 <..< t}) (u, x) *\<^sub>R (sin x * exp (-(u * x))))"
+ also have "\<dots> = (LBINT x. (LBINT u. indicator ({0<..} \<times> {0 <..< t}) (u, x) *\<^sub>R (sin x * exp (-(u * x)))))"
apply (subst interval_integral_Ioi)
unfolding set_lebesgue_integral_def by(simp_all add: indicator_times ac_simps )
- also have "\<dots> = LBINT u. (LBINT x. indicator ({0<..} \<times> {0 <..< t}) (u, x) *\<^sub>R (sin x * exp (-(u * x))))"
+ also have "\<dots> = (LBINT u. (LBINT x. indicator ({0<..} \<times> {0 <..< t}) (u, x) *\<^sub>R (sin x * exp (-(u * x)))))"
proof (intro lborel_pair.Fubini_integral[symmetric] lborel_pair.Fubini_integrable)
show "(\<lambda>(x, y). indicator ({0<..} \<times> {0<..<t}) (y, x) *\<^sub>R (sin x * exp (- (y * x))))
\<in> borel_measurable (lborel \<Otimes>\<^sub>M lborel)" (is "?f \<in> borel_measurable _")
by measurable
- have "AE x in lborel. indicator {0..t} x *\<^sub>R abs (sinc x) = LBINT y. norm (?f (x, y))"
+ have "AE x in lborel. indicator {0..t} x *\<^sub>R abs (sinc x) = (LBINT y. norm (?f (x, y)))"
using AE_lborel_singleton[of 0] AE_lborel_singleton[of t]
proof eventually_elim
fix x :: real assume x: "x \<noteq> 0" "x \<noteq> t"
- have "LBINT y. \<bar>indicator ({0<..} \<times> {0<..<t}) (y, x) *\<^sub>R (sin x * exp (- (y * x)))\<bar> =
- LBINT y. \<bar>sin x\<bar> * exp (- (y * x)) * indicator {0<..} y * indicator {0<..<t} x"
+ have "(LBINT y. \<bar>indicator ({0<..} \<times> {0<..<t}) (y, x) *\<^sub>R (sin x * exp (- (y * x)))\<bar>) =
+ (LBINT y. \<bar>sin x\<bar> * exp (- (y * x)) * indicator {0<..} y * indicator {0<..<t} x)"
by (intro Bochner_Integration.integral_cong) (auto split: split_indicator simp: abs_mult)
also have "\<dots> = \<bar>sin x\<bar> * indicator {0<..<t} x * (LBINT y=0..\<infinity>. exp (- (y * x)))"
by (cases "x > 0")
@@ -303,7 +303,7 @@
by (cases "x > 0") (auto simp add: LBINT_I0i_exp_mscale)
also have "\<dots> = indicator {0..t} x *\<^sub>R \<bar>sinc x\<bar>"
using x by (simp add: field_simps split: split_indicator)
- finally show "indicator {0..t} x *\<^sub>R abs (sinc x) = LBINT y. norm (?f (x, y))"
+ finally show "indicator {0..t} x *\<^sub>R abs (sinc x) = (LBINT y. norm (?f (x, y)))"
by simp
qed
moreover have "integrable lborel (\<lambda>x. indicat_real {0..t} x *\<^sub>R \<bar>sinc x\<bar>)"
@@ -316,11 +316,11 @@
then show "AE x in lborel. integrable lborel (\<lambda>y. ?f (x, y))"
by (intro AE_I2) (auto simp: indicator_times set_integrable_def split: split_indicator)
qed
- also have "... = LBINT u=0..\<infinity>. (LBINT x=0..t. exp (-(u * x)) * sin x)"
+ also have "... = (LBINT u=0..\<infinity>. (LBINT x=0..t. exp (-(u * x)) * sin x))"
using \<open>0\<le>t\<close>
by (auto simp: interval_lebesgue_integral_def set_lebesgue_integral_def zero_ereal_def ac_simps
split: split_indicator intro!: Bochner_Integration.integral_cong)
- also have "\<dots> = LBINT u=0..\<infinity>. 1 / (1 + u\<^sup>2) - 1 / (1 + u\<^sup>2) * (exp (- (u * t)) * (u * sin t + cos t))"
+ also have "\<dots> = (LBINT u=0..\<infinity>. 1 / (1 + u\<^sup>2) - 1 / (1 + u\<^sup>2) * (exp (- (u * t)) * (u * sin t + cos t)))"
by (auto simp: divide_simps LBINT_I0c_exp_mscale_sin intro!: interval_integral_cong)
also have "... = pi / 2 - (LBINT u=0..\<infinity>. exp (- (u * t)) * (u * sin t + cos t) / (1 + u^2))"
using Si_at_top_integrable[OF \<open>0\<le>t\<close>] by (simp add: integrable_I0i_1_div_plus_square LBINT_I0i_1_div_plus_square)
@@ -371,8 +371,7 @@
by (rule interval_integral_discrete_difference[of "{0}"]) auto
finally have "(LBINT t=ereal 0..T. sin (t * \<theta>) / t) = (LBINT t=ereal 0..T * \<theta>. sin t / t)"
by simp
- hence "LBINT x. indicator {0<..<T} x * sin (x * \<theta>) / x =
- LBINT x. indicator {0<..<T * \<theta>} x * sin x / x"
+ hence "(LBINT x. indicator {0<..<T} x * sin (x * \<theta>) / x) = (LBINT x. indicator {0<..<T * \<theta>} x * sin x / x)"
using assms \<open>0 < \<theta>\<close> unfolding interval_lebesgue_integral_def einterval_eq zero_ereal_def
by (auto simp: ac_simps set_lebesgue_integral_def)
} note aux1 = this
@@ -390,7 +389,7 @@
by (rule interval_integral_discrete_difference[of "{0}"]) auto
finally have "(LBINT t=ereal 0..T. sin (t * -\<theta>) / t) = (LBINT t=ereal 0..T * -\<theta>. sin t / t)"
by simp
- hence "LBINT x. indicator {0<..<T} x * sin (x * \<theta>) / x =
+ hence "(LBINT x. indicator {0<..<T} x * sin (x * \<theta>) / x) =
- (LBINT x. indicator {0<..<- (T * \<theta>)} x * sin x / x)"
using assms \<open>0 > \<theta>\<close> unfolding interval_lebesgue_integral_def einterval_eq zero_ereal_def
by (auto simp add: field_simps mult_le_0_iff set_lebesgue_integral_def split: if_split_asm)
--- a/src/HOL/Tools/Nitpick/kodkod.scala Wed Feb 14 16:25:41 2024 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.scala Thu Feb 15 08:25:25 2024 +0100
@@ -42,7 +42,7 @@
): Result = {
/* executor */
- val pool_size = if (max_threads == 0) Isabelle_Thread.max_threads() else max_threads
+ val pool_size = if (max_threads == 0) Multithreading.max_threads() else max_threads
val executor: ThreadPoolExecutor =
new ThreadPoolExecutor(pool_size, pool_size, 0L, TimeUnit.MILLISECONDS,
new LinkedBlockingQueue[Runnable], new ThreadPoolExecutor.CallerRunsPolicy)
--- a/src/Pure/Concurrent/isabelle_thread.scala Wed Feb 14 16:25:41 2024 +0100
+++ b/src/Pure/Concurrent/isabelle_thread.scala Thu Feb 15 08:25:25 2024 +0100
@@ -72,13 +72,8 @@
/* thread pool */
- def max_threads(): Int = {
- val m = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0
- if (m > 0) m else (Host.num_cpus() max 1) min 8
- }
-
lazy val pool: ThreadPoolExecutor = {
- val n = max_threads()
+ val n = Multithreading.max_threads()
val executor =
new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable])
executor.setThreadFactory(
--- a/src/Pure/Concurrent/multithreading.ML Wed Feb 14 16:25:41 2024 +0100
+++ b/src/Pure/Concurrent/multithreading.ML Thu Feb 15 08:25:25 2024 +0100
@@ -1,11 +1,14 @@
(* Title: Pure/Concurrent/multithreading.ML
Author: Makarius
-Multithreading in Poly/ML (cf. polyml/basis/Thread.sml).
+Multithreading in Poly/ML, see also
+ - $ML_SOURCES/basis/Thread.sml: numPhysicalProcessors
+ - $ML_SOURCES/libpolyml/processes.cpp: PolyThreadNumPhysicalProcessors
*)
signature MULTITHREADING =
sig
+ val num_processors: unit -> int
val max_threads: unit -> int
val max_threads_update: int -> unit
val parallel_proofs: int ref
@@ -20,15 +23,18 @@
structure Multithreading: MULTITHREADING =
struct
-(* max_threads *)
-
-local
+(* physical processors *)
fun num_processors () =
(case Thread.Thread.numPhysicalProcessors () of
SOME n => n
| NONE => Thread.Thread.numProcessors ());
+
+(* max_threads *)
+
+local
+
fun max_threads_result m =
if Thread_Data.is_virtual then 1
else if m > 0 then m
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/multithreading.scala Thu Feb 15 08:25:25 2024 +0100
@@ -0,0 +1,49 @@
+/* Title: Pure/Concurrent/multithreading.scala
+ Author: Makarius
+
+Multithreading in Isabelle/Scala.
+*/
+
+package isabelle
+
+
+object Multithreading {
+ /* physical processors */
+
+ // slightly different from Poly/ML (more accurate)
+ def num_processors(ssh: SSH.System = SSH.Local): Int =
+ if (ssh.isabelle_platform.is_macos) {
+ val result = ssh.execute("sysctl -n hw.physicalcpu").check
+ Library.trim_line(result.out) match {
+ case Value.Int(n) => n
+ case _ => 1
+ }
+ }
+ else {
+ val Physical = """^\s*physical id\s*:\s*(\d+)\s*$""".r
+ val Cores = """^\s*cpu cores\s*:\s*(\d+)\s*$""".r
+
+ var physical: Option[Int] = None
+ var physical_cores = Map.empty[Int, Int]
+
+ val result = ssh.execute("cat /proc/cpuinfo").check
+ for (line <- Library.trim_split_lines(result.out)) {
+ line match {
+ case Physical(Value.Int(i)) => physical = Some(i)
+ case Cores(Value.Int(i))
+ if physical.isDefined && !physical_cores.isDefinedAt(physical.get) =>
+ physical_cores = physical_cores + (physical.get -> i)
+ case _ =>
+ }
+ }
+ physical_cores.valuesIterator.sum.max(1)
+ }
+
+
+ /* max_threads */
+
+ def max_threads(): Int = {
+ val m = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0
+ if (m > 0) m else (num_processors() max 1) min 8
+ }
+}
--- a/src/Pure/System/benchmark.scala Wed Feb 14 16:25:41 2024 +0100
+++ b/src/Pure/System/benchmark.scala Thu Feb 15 08:25:25 2024 +0100
@@ -98,7 +98,7 @@
progress.echo(
"Finished benchmark in " + timing.message + ". Score: " + String.format("%.2f", score))
- Host.write_info(db, Host.Info.gather(hostname, score = Some(score)))
+ Host.write_info(db, Host.Info.init(hostname = hostname, score = Some(score)))
}
}
}
--- a/src/Pure/System/host.scala Wed Feb 14 16:25:41 2024 +0100
+++ b/src/Pure/System/host.scala Thu Feb 15 08:25:25 2024 +0100
@@ -122,28 +122,22 @@
}
catch { case ERROR(_) => None }
- def num_cpus(ssh: SSH.System = SSH.Local): Int =
- if (ssh.is_local) Runtime.getRuntime.availableProcessors
- else {
- val command =
- if (ssh.isabelle_platform.is_macos) "sysctl -n hw.ncpu" else "nproc"
- val result = ssh.execute(command).check
- Library.trim_line(result.out) match {
- case Value.Int(n) => n
- case _ => 1
- }
- }
-
object Info {
- def gather(hostname: String, ssh: SSH.System = SSH.Local, score: Option[Double] = None): Info =
- Info(hostname, numa_nodes(ssh = ssh), num_cpus(ssh = ssh), score)
+ def init(
+ hostname: String = SSH.LOCAL,
+ ssh: SSH.System = SSH.Local,
+ score: Option[Double] = None
+ ): Info = Info(hostname, numa_nodes(ssh = ssh), Multithreading.num_processors(ssh = ssh), score)
}
sealed case class Info(
hostname: String,
numa_nodes: List[Int],
num_cpus: Int,
- benchmark_score: Option[Double])
+ benchmark_score: Option[Double]
+ ) {
+ override def toString: String = hostname
+ }
/* shuffling of NUMA nodes */