# HG changeset patch
# User wenzelm
# Date 1755681433 -7200
# Node ID 84f26fbac4c4cf56a01bdededa1a10ff4b544aef
# Parent  d35875d530a2284c41f8bf02281196d7fc291c4d# Parent  fa6c4ad21a240aa7dab2bf588f254e492b2b5cdb
merged

diff -r fa6c4ad21a24 -r 84f26fbac4c4 src/HOL/Analysis/Interval_Integral.thy
--- a/src/HOL/Analysis/Interval_Integral.thy	Sat Aug 16 16:34:41 2025 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy	Wed Aug 20 11:17:13 2025 +0200
@@ -402,6 +402,14 @@
   "a \<le> b \<Longrightarrow> \<bar>a\<bar> < \<infinity> ==> \<bar>b\<bar> < \<infinity> \<Longrightarrow> (LBINT x=a..b. f x) = (LBINT x : {real_of_ereal a <..< real_of_ereal b}. f x)"
   by (auto simp: interval_lebesgue_integral_def einterval_iff)
 
+lemma has_bochner_interval_integral_iff:
+  assumes "a\<le>b"
+  shows "has_bochner_integral (restrict_space lborel {a..b}) f x 
+      \<longleftrightarrow> set_integrable lborel {a..b} f \<and> (LBINT u=a..b. f u) = x"
+  using assms
+  by (simp add: has_bochner_integral_iff integral_restrict_space interval_integral_Icc
+      set_integrable_eq set_lebesgue_integral_def)
+
 lemma interval_integral_discrete_difference:
   fixes f :: "real \<Rightarrow> 'b::{banach, second_countable_topology}" and a b :: ereal
   assumes "countable X"
diff -r fa6c4ad21a24 -r 84f26fbac4c4 src/HOL/Analysis/Set_Integral.thy
--- a/src/HOL/Analysis/Set_Integral.thy	Sat Aug 16 16:34:41 2025 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy	Wed Aug 20 11:17:13 2025 +0200
@@ -33,10 +33,11 @@
 
 section \<open>Basic properties\<close>
 
-(*
-lemma indicator_abs_eq: "\<And>A x. \<bar>indicator A x\<bar> = ((indicator A x) :: real)"
-  by (auto simp add: indicator_def)
-*)
+lemma set_integrable_eq:
+  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+  assumes "\<Omega> \<inter> space M \<in> sets M"
+  shows "set_integrable M \<Omega> f = integrable (restrict_space M \<Omega>) f"
+  by (meson assms integrable_restrict_space set_integrable_def)
 
 lemma set_integrable_cong:
   assumes "M = M'" "A = A'" "\<And>x. x \<in> A \<Longrightarrow> f x = f' x"
diff -r fa6c4ad21a24 -r 84f26fbac4c4 src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Aug 16 16:34:41 2025 +0200
+++ b/src/HOL/List.thy	Wed Aug 20 11:17:13 2025 +0200
@@ -798,11 +798,9 @@
                 val lhs = Thm.term_of redex
                 val rhs = HOLogic.mk_Collect ("x", rT, inner_t)
                 val rewrite_rule_t = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
-              in
-                SOME
-                  ((Goal.prove ctxt [] [] rewrite_rule_t
-                    (fn {context = ctxt', ...} => tac ctxt' (rev Tis))) RS @{thm eq_reflection})
-              end))
+                val eq_thm = Goal.norm_result ctxt (Goal.prove_internal ctxt []
+                  (Thm.cterm_of ctxt rewrite_rule_t) (fn _ => tac ctxt (rev Tis)))
+              in SOME (eq_thm RS @{thm eq_reflection}) end))
   in
     make_inner_eqs [] [] [] (dest_set (Thm.term_of redex))
   end