# HG changeset patch # User desharna # Date 1707981925 -3600 # Node ID 8836386d6e3f0cc67a03033ff3fc1193e110b3c0 # Parent 97612262718aadb099a62b5016b9248feb10a9f3# Parent ad29777e8746b6422f582ff15936a36c383a4fba merged diff -r 97612262718a -r 8836386d6e3f NEWS --- 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, \, 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. diff -r 97612262718a -r 8836386d6e3f etc/build.props --- 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 \ diff -r 97612262718a -r 8836386d6e3f src/HOL/Analysis/Bochner_Integration.thy --- 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 "\i. norm (s i x) \ w x" "(\i. s i x) \ f x" "0 \ w x" then show "ennreal (norm (f x)) \ ennreal (w x)" - by (intro LIMSEQ_le_const2[where X="\i. ennreal (norm (s i x))"]) (auto intro: tendsto_intros) + by (metis LIMSEQ_le_const2 ennreal_leI tendsto_norm) qed with w show "(\\<^sup>+ x. ennreal (norm (f x)) \M) < \" by auto qed fact diff -r 97612262718a -r 8836386d6e3f src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy --- 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 \ '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 = "\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 \ '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 :: "_ \ 'a :: {banach, second_countable_topology}" - shows "set_integrable M k f \ norm (LINT x:k|M. f x) \ LINT x:k|M. norm (f x)" + shows "set_integrable M k f \ norm (LINT x:k|M. f x) \ (LINT x:k|M. norm (f x))" using integral_norm_bound[of M "\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: "\i j. i \ I \ j \ I \ AE x in M. (x \ A i \ x \ A j) \ i = j" and [measurable]: "\i. i \ I \ A i \ sets M" and f: "\i. i \ I \ set_integrable M (A i) f" - shows "LINT x:(\i\I. A i)|M. f x = (\i\I. LINT x:A i|M. f x)" + shows "(LINT x:(\i\I. A i)|M. f x) = (\i\I. LINT x:A i|M. f x)" using \finite I\ 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 - \x. (f x * G x) * indicator {a .. b} x \lborel" proof- have "(\x. (F x * g x + f x * G x) * indicator {a .. b} x \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 "... = (\x. (F x * g x) * indicator {a .. b} x \lborel) + \x. (f x * G x) * indicator {a .. b} x \lborel" proof (intro Bochner_Integration.integral_add borel_integrable_atLeastAtMost cont_f cont_g continuous_intros) diff -r 97612262718a -r 8836386d6e3f src/HOL/Analysis/Interval_Integral.thy --- 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 \ einterval a b}. f (- x) = LBINT x:einterval (- b) (- a). f (- x)" + have "(LBINT x:{x. - x \ 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 (\x. c)" and "LBINT x=a..b. c = c * (b - a)" + shows "interval_lebesgue_integrable lborel a b (\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: "\x. a \ x \ x \ b \ (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: "\x. a \ x \ x \ b \ (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} (\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 \a \ b\ 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)" diff -r 97612262718a -r 8836386d6e3f src/HOL/Analysis/Lebesgue_Integral_Substitution.thy --- 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 \{u'..v'} \ {a..b}\ eucl_ivals(5) set_integrable_def sets_lborel u'v'(1)) hence "(\\<^sup>+x. ennreal (g' x) * indicator ({a..b} \ g-` {u..v}) x \lborel) = - LBINT x:{a..b} \ g-`{u..v}. g' x" + (LBINT x:{a..b} \ 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} \ g-`{u..v}. g' x = v - u" + have "(LBINT x:{a..b} \ g-`{u..v}. g' x) = v - u" by (simp add: u'v' interval_integral_Icc \u \ v\) finally have "(\\<^sup>+ x. ennreal (g' x) * indicator ({a..b} \ g -` {u..v}) x \lborel) = ennreal (v - u)" . @@ -130,12 +130,12 @@ (simp split: split_indicator) also have "... = \\<^sup>+ x. indicator (g-`A \ {a..b}) x * ennreal (g' x * indicator {a..b} x) \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 ... = \\<^sup>+ x. g' x * indicator {a..b} x \lborel" + also have "ennreal ... = (\\<^sup>+ x. g' x * indicator {a..b} x \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: "(\x. -f x * indicator {g a..g b} x) \ 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 (\\<^sup>+ x. ennreal (f x) * indicator {g a..g b} x \lborel) - enn2real (\\<^sup>+ x. ennreal (- (f x)) * indicator {g a..g b} x \lborel)" using integrable unfolding set_integrable_def diff -r 97612262718a -r 8836386d6e3f src/HOL/Analysis/Set_Integral.thy --- 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 \ 'a set \ 'a measure \ real \ 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 (\x. f)" @@ -39,11 +39,11 @@ syntax "_lebesgue_borel_integral" :: "pttrn \ real \ real" - ("(2LBINT _./ _)" [0,60] 60) + ("(2LBINT _./ _)" [0,60] 10) syntax "_set_lebesgue_borel_integral" :: "pttrn \ real set \ real \ 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 \ sets M" "f \ borel_measurable M" "g \ borel_measurable M" assumes "AE x \ 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 :: "_ \ _ :: {banach, second_countable_topology}" assumes "set_integrable M A f" "set_integrable M A g" shows "set_integrable M A (\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 (\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 (\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 \ LINT x:A|M. - f x = - (LINT x:A|M. f x)" +lemma set_integral_uminus: "set_integrable M A f \ (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 \ B = {}" and "set_integrable M A f" and "set_integrable M B f" -shows "LINT x:A\B|M. f x = (LINT x:A|M. f x) + (LINT x:B|M. f x)" +shows "(LINT x:A\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 :: "_ \ _ :: {banach, second_countable_topology}" assumes "set_borel_measurable M A f" "set_borel_measurable M B f" and ae: "AE x in M. x \ A \ x \ 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. \ (x \ A \ x \ B)" and [measurable]: "A \ sets M" "B \ sets M" and "set_integrable M A f" and "set_integrable M B f" - shows "LINT x:A\B|M. f x = (LINT x:A|M. f x) + (LINT x:B|M. f x)" + shows "(LINT x:A\B|M. f x) = (LINT x:A|M. f x) + (LINT x:B|M. f x)" proof - have f: "set_integrable M (A \ B) f" by (intro set_integrable_Un assms) then have f': "set_borel_measurable M (A \ B) f" using integrable_iff_bounded set_borel_measurable_def set_integrable_def by blast - have "LINT x:A\B|M. f x = LINT x:(A - A \ B) \ (B - A \ B)|M. f x" + have "(LINT x:A\B|M. f x) = (LINT x:(A - A \ B) \ (B - A \ B)|M. f x)" proof (rule set_integral_cong_set) show "AE x in M. (x \ A - A \ B \ (B - A \ B)) = (x \ A \ B)" using ae by auto @@ -420,11 +419,11 @@ and intgbl: "\i::nat. set_integrable M (A i) f" and lim: "(\i::nat. LINT x:A i|M. f x) \ l" shows "set_integrable M (\i. A i) f" - unfolding set_integrable_def + unfolding set_integrable_def apply (rule integrable_monotone_convergence[where f = "\i::nat. \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 \mono A\ apply (auto simp: mono_def nneg split: split_indicator) [] proof (rule AE_I2) { fix x assume "x \ space M" @@ -432,18 +431,16 @@ proof cases assume "\i. x \ A i" then obtain i where "x \ A i" .. - then have *: "eventually (\i. x \ A i) sequentially" + then have "\\<^sub>F i in sequentially. x \ A i" using \x \ A i\ \mono A\ 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 "\\<^sub>F i in sequentially. indicat_real (A i) x *\<^sub>R f x = indicat_real (\ (range A)) x *\<^sub>R f x" + by fastforce + then show ?thesis + by (intro tendsto_eventually) qed auto } then show "(\x. indicator (\i. A i) x *\<^sub>R f x) \ 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]: "\i::nat. A i \ sets M" and disj: "\i j. i \ j \ A i \ A j = {}" and intgbl: "set_integrable M (\i. A i) f" - shows "LINT x:(\i. A i)|M. f x = (\i. (LINT x:(A i)|M. f x))" + shows "(LINT x:(\i. A i)|M. f x) = (\i. (LINT x:(A i)|M. f x))" unfolding set_lebesgue_integral_def proof (subst integral_suminf[symmetric]) show int_A: "integrable M (\x. indicat_real (A i) x *\<^sub>R f x)" for i @@ -503,7 +500,7 @@ fixes f :: "_ \ 'a :: {banach, second_countable_topology}" assumes [measurable]: "\i. A i \ sets M" and A: "incseq A" and intgbl: "set_integrable M (\i. A i) f" -shows "(\i. LINT x:(A i)|M. f x) \ LINT x:(\i. A i)|M. f x" +shows "(\i. LINT x:(A i)|M. f x) \ (LINT x:(\i. A i)|M. f x)" unfolding set_lebesgue_integral_def proof (intro integral_dominated_convergence[where w="\x. indicator (\i. A i) x *\<^sub>R norm (f x)"]) have int_A: "\i. set_integrable M (A i) f" @@ -528,7 +525,7 @@ fixes f :: "_ \ 'a :: {banach, second_countable_topology}" assumes [measurable]: "\i. A i \ sets M" and A: "decseq A" and int0: "set_integrable M (A 0) f" - shows "(\i::nat. LINT x:(A i)|M. f x) \ LINT x:(\i. A i)|M. f x" + shows "(\i::nat. LINT x:(A i)|M. f x) \ (LINT x:(\i. A i)|M. f x)" unfolding set_lebesgue_integral_def proof (rule integral_dominated_convergence) have int_A: "\i. set_integrable M (A i) f" @@ -580,7 +577,7 @@ syntax "_ascii_complex_lebesgue_integral" :: "pttrn \ 'a measure \ real \ real" - ("(3CLINT _|_. _)" [0,110,60] 60) + ("(3CLINT _|_. _)" [0,110,60] 10) translations "CLINT x|M. f" == "CONST complex_lebesgue_integral M (\x. f)" @@ -614,7 +611,7 @@ syntax "_ascii_complex_set_lebesgue_integral" :: "pttrn \ 'a set \ 'a measure \ real \ 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 (\x. f)" @@ -633,10 +630,10 @@ syntax "_set_nn_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal" -("(\\<^sup>+((_)\(_)./ _)/\_)" [0,60,110,61] 60) +("(\\<^sup>+((_)\(_)./ _)/\_)" [0,60,110,61] 10) "_set_lebesgue_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal" -("(\((_)\(_)./ _)/\_)" [0,60,110,61] 60) +("(\((_)\(_)./ _)/\_)" [0,60,110,61] 10) translations "\\<^sup>+x \ A. f \M" == "CONST set_nn_integral M A (\x. f)" diff -r 97612262718a -r 8836386d6e3f src/HOL/Bit_Operations.thy --- 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 @@ \bit (a mod 2) n \ n = 0 \ odd a\ by (simp add: mod_2_eq_odd bit_simps) -lemma bit_disjunctive_add_iff: - \bit (a + b) n \ bit a n \ bit b n\ - if \\n. \ bit a n \ \ bit b n\ -proof (cases \possible_bit TYPE('a) n\) - 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: \even a \ even b\ - by (auto simp add: bit_0) - have bit: \\ bit (a div 2) n \ \ bit (b div 2) n\ for n - using Suc.prems(1) [of \Suc n\] by (simp add: bit_Suc) - from Suc.prems(2) have \possible_bit TYPE('a) (Suc n)\ \possible_bit TYPE('a) n\ - by (simp_all add: possible_bit_less_imp) - have \a + b = (a div 2 * 2 + a mod 2) + (b div 2 * 2 + b mod 2)\ - using div_mult_mod_eq [of a 2] div_mult_mod_eq [of b 2] by simp - also have \\ = of_bool (odd a \ odd b) + 2 * (a div 2 + b div 2)\ - using even by (auto simp add: algebra_simps mod2_eq_if) - finally have \bit ((a + b) div 2) n \ bit (a div 2 + b div 2) n\ - using \possible_bit TYPE('a) (Suc n)\ by simp (simp_all flip: bit_Suc add: bit_double_iff possible_bit_def) - also have \\ \ bit (a div 2) n \ bit (b div 2) n\ - using bit \possible_bit TYPE('a) n\ 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 @@ \even (a OR b) \ even a \ even b\ using bit_or_iff [of a b 0] by (auto simp add: bit_0) -lemma disjunctive_add: - \a + b = a OR b\ if \\n. \ bit a n \ \ bit b n\ - by (rule bit_eqI) (use that in \simp add: bit_disjunctive_add_iff bit_or_iff\) - lemma even_xor_iff: \even (a XOR b) \ (even a \ even b)\ using bit_xor_iff [of a b 0] by (auto simp add: bit_0) @@ -1283,13 +1245,59 @@ \take_bit n a = (\k = 0.. by (simp flip: horner_sum_bit_eq_take_bit add: horner_sum_eq_sum push_bit_eq_mult) +lemma disjunctive_xor_eq_or: + \a XOR b = a OR b\ if \a AND b = 0\ + using that by (auto simp add: bit_eq_iff bit_simps) + +lemma disjunctive_add_eq_or: + \a + b = a OR b\ if \a AND b = 0\ +proof (rule bit_eqI) + fix n + assume \possible_bit TYPE('a) n\ + moreover from that have \\n. \ bit (a AND b) n\ + by simp + then have \\n. \ bit a n \ \ bit b n\ + by (simp add: bit_simps) + ultimately show \bit (a + b) n \ bit (a OR b) n\ + 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: \even a \ even b\ + by (auto simp add: bit_0) + have bit: \\ bit (a div 2) n \ \ bit (b div 2) n\ for n + using Suc.prems(2) [of \Suc n\] by (simp add: bit_Suc) + from Suc.prems have \possible_bit TYPE('a) n\ + using possible_bit_less_imp by force + with \\n. \ bit (a div 2) n \ \ bit (b div 2) n\ Suc.IH [of \a div 2\ \b div 2\] + have IH: \bit (a div 2 + b div 2) n \ bit (a div 2 OR b div 2) n\ + by (simp add: bit_Suc) + have \a + b = (a div 2 * 2 + a mod 2) + (b div 2 * 2 + b mod 2)\ + using div_mult_mod_eq [of a 2] div_mult_mod_eq [of b 2] by simp + also have \\ = of_bool (odd a \ odd b) + 2 * (a div 2 + b div 2)\ + using even by (auto simp add: algebra_simps mod2_eq_if) + finally have \bit ((a + b) div 2) n \ bit (a div 2 + b div 2) n\ + using \possible_bit TYPE('a) (Suc n)\ by simp (simp_all flip: bit_Suc add: bit_double_iff possible_bit_def) + also have \\ \ bit (a div 2 OR b div 2) n\ + by (rule IH) + finally show ?case + by (simp add: bit_simps flip: bit_Suc) + qed +qed + +lemma disjunctive_add_eq_xor: + \a + b = a XOR b\ if \a AND b = 0\ + using that by (simp add: disjunctive_add_eq_or disjunctive_xor_eq_or) + lemma set_bit_eq: \set_bit n a = a + of_bool (\ bit a n) * 2 ^ n\ proof - - have \set_bit n a = a OR of_bool (\ bit a n) * 2 ^ n\ - by (rule bit_eqI) (auto simp add: bit_simps) + have \a AND of_bool (\ bit a n) * 2 ^ n = 0\ + 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 @@ \a AND b = - 1 \ a = - 1 \ b = - 1\ by (auto simp: bit_eq_iff bit_simps) -lemma disjunctive_diff: - \a - b = a AND NOT b\ if \\n. bit b n \ bit a n\ +lemma disjunctive_and_not_eq_xor: + \a AND NOT b = a XOR b\ if \NOT a AND b = 0\ + using that by (auto simp add: bit_eq_iff bit_simps) + +lemma disjunctive_diff_eq_and_not: + \a - b = a AND NOT b\ if \NOT a AND b = 0\