merged
authordesharna
Wed, 17 May 2023 09:00:04 +0200
changeset 78105 ab8310c0e6d9
parent 78104 8122e865687e (current diff)
parent 78037 37894dff0111 (diff)
child 78106 6fe9cdf547c4
merged
--- a/etc/options	Tue May 16 23:41:20 2023 +0200
+++ b/etc/options	Wed May 17 09:00:04 2023 +0200
@@ -111,6 +111,15 @@
 public option timeout_scale : real = 1.0 for build
   -- "scale factor for timeout in Isabelle/ML and session build"
 
+option context_data_timing : bool = false for build
+  -- "timing for context data operations"
+
+option context_theory_tracing : bool = false for build
+  -- "tracing of persistent theory values within ML heap"
+
+option context_proof_tracing : bool = false for build
+  -- "tracing of persistent Proof.context values within ML heap"
+
 
 section "Detail of Proof Checking"
 
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Tue May 16 23:41:20 2023 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Wed May 17 09:00:04 2023 +0200
@@ -234,7 +234,7 @@
   notes semi_hom_mult = semi_hom_mult [OF semi_homh]
 
 thm semi_hom_loc.semi_hom_mult
-(* unspecified, attribute not applied in backgroud theory !!! *)
+(* unspecified, attribute not applied in background theory !!! *)
 
 lemma (in semi_hom_loc) \<open>h(prod(x, y)) = sum(h(x), h(y))\<close>
   by (rule semi_hom_mult)
--- a/src/HOL/Analysis/Abstract_Topological_Spaces.thy	Tue May 16 23:41:20 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Topological_Spaces.thy	Wed May 17 09:00:04 2023 +0200
@@ -71,69 +71,6 @@
   by (simp add: Hausdorff_imp_t1_space connectedin_imp_perfect_gen)
 
 
-proposition connected_space_prod_topology:
-   "connected_space(prod_topology X Y) \<longleftrightarrow>
-    topspace(prod_topology X Y) = {} \<or> connected_space X \<and> connected_space Y" (is "?lhs=?rhs")
-proof (cases "topspace(prod_topology X Y) = {}")
-  case True
-  then show ?thesis
-    using connected_space_topspace_empty by blast
-next
-  case False
-  then have nonempty: "topspace X \<noteq> {}" "topspace Y \<noteq> {}"
-    by force+
-  show ?thesis 
-  proof
-    assume ?lhs
-    then show ?rhs
-      by (meson connected_space_quotient_map_image nonempty quotient_map_fst quotient_map_snd)
-  next
-    assume ?rhs
-    then have conX: "connected_space X" and conY: "connected_space Y"
-      using False by blast+
-    have False
-      if "openin (prod_topology X Y) U" and "openin (prod_topology X Y) V"
-        and UV: "topspace X \<times> topspace Y \<subseteq> U \<union> V" "U \<inter> V = {}" 
-        and "U \<noteq> {}" and "V \<noteq> {}"
-      for U V
-    proof -
-      have Usub: "U \<subseteq> topspace X \<times> topspace Y" and Vsub: "V \<subseteq> topspace X \<times> topspace Y"
-        using that by (metis openin_subset topspace_prod_topology)+
-      obtain a b where ab: "(a,b) \<in> U" and a: "a \<in> topspace X" and b: "b \<in> topspace Y"
-        using \<open>U \<noteq> {}\<close> Usub by auto
-      have "\<not> topspace X \<times> topspace Y \<subseteq> U"
-        using Usub Vsub \<open>U \<inter> V = {}\<close> \<open>V \<noteq> {}\<close> by auto
-      then obtain x y where x: "x \<in> topspace X" and y: "y \<in> topspace Y" and "(x,y) \<notin> U"
-        by blast
-      have oX: "openin X {x \<in> topspace X. (x,y) \<in> U}" "openin X {x \<in> topspace X. (x,y) \<in> V}"
-       and oY: "openin Y {y \<in> topspace Y. (a,y) \<in> U}" "openin Y {y \<in> topspace Y. (a,y) \<in> V}"
-        by (force intro: openin_continuous_map_preimage [where Y = "prod_topology X Y"] 
-            simp: that continuous_map_pairwise o_def x y a)+
-      have 1: "topspace Y \<subseteq> {y \<in> topspace Y. (a,y) \<in> U} \<union> {y \<in> topspace Y. (a,y) \<in> V}"
-        using a that(3) by auto
-      have 2: "{y \<in> topspace Y. (a,y) \<in> U} \<inter> {y \<in> topspace Y. (a,y) \<in> V} = {}"
-        using that(4) by auto
-      have 3: "{y \<in> topspace Y. (a,y) \<in> U} \<noteq> {}"
-        using ab b by auto
-      have 4: "{y \<in> topspace Y. (a,y) \<in> V} \<noteq> {}"
-      proof -
-        show ?thesis
-          using connected_spaceD [OF conX oX] UV \<open>(x,y) \<notin> U\<close> a x y
-                disjoint_iff_not_equal by blast
-      qed
-      show ?thesis
-        using connected_spaceD [OF conY oY 1 2 3 4] by auto
-    qed
-    then show ?lhs
-      unfolding connected_space_def topspace_prod_topology by blast 
-  qed
-qed
-
-lemma connectedin_Times:
-   "connectedin (prod_topology X Y) (S \<times> T) \<longleftrightarrow>
-        S = {} \<or> T = {} \<or> connectedin X S \<and> connectedin Y T"
-  by (force simp: connectedin_def subtopology_Times connected_space_prod_topology)
-
 
 subsection\<open>The notion of "separated between" (complement of "connected between)"\<close>
 
--- a/src/HOL/Analysis/Abstract_Topology.thy	Tue May 16 23:41:20 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Wed May 17 09:00:04 2023 +0200
@@ -296,6 +296,10 @@
   unfolding closedin_def topspace_subtopology
   by (auto simp: openin_subtopology)
 
+lemma closedin_subset_topspace:
+   "\<lbrakk>closedin X S; S \<subseteq> T\<rbrakk> \<Longrightarrow> closedin (subtopology X T) S"
+  using closedin_subtopology by fastforce
+
 lemma closedin_relative_to:
    "(closedin X relative_to S) = closedin (subtopology X S)"
   by (force simp: relative_to_def closedin_subtopology)
@@ -3378,6 +3382,10 @@
   qed
 qed
 
+lemma connected_space_quotient_map_image:
+   "\<lbrakk>quotient_map X X' q; connected_space X\<rbrakk> \<Longrightarrow> connected_space X'"
+  by (metis connectedin_continuous_map_image connectedin_topspace quotient_imp_continuous_map quotient_imp_surjective_map)
+
 lemma homeomorphic_connected_space:
      "X homeomorphic_space Y \<Longrightarrow> connected_space X \<longleftrightarrow> connected_space Y"
   unfolding homeomorphic_space_def homeomorphic_maps_def
--- a/src/HOL/Analysis/Abstract_Topology_2.thy	Tue May 16 23:41:20 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy	Wed May 17 09:00:04 2023 +0200
@@ -1639,4 +1639,53 @@
      (\<lambda>x. x / (1 + \<bar>x\<bar>))  (\<lambda>y. y / (1 - \<bar>y\<bar>))"
   by (force simp: homeomorphic_maps_def continuous_map_real_shrink continuous_on_real_grow divide_simps)
 
+lemma real_shrink_Galois:
+  fixes x::real
+  shows "(x / (1 + \<bar>x\<bar>) = y) \<longleftrightarrow> (\<bar>y\<bar> < 1 \<and> y / (1 - \<bar>y\<bar>) = x)"
+  using real_grow_shrink by (fastforce simp add: distrib_left)
+
+lemma real_shrink_lt:
+  fixes x::real
+  shows "x / (1 + \<bar>x\<bar>) < y / (1 + \<bar>y\<bar>) \<longleftrightarrow> x < y"
+  using zero_less_mult_iff [of x y] by (auto simp: field_simps abs_if not_less)
+
+lemma real_shrink_le:
+  fixes x::real
+  shows "x / (1 + \<bar>x\<bar>) \<le> y / (1 + \<bar>y\<bar>) \<longleftrightarrow> x \<le> y"
+  by (meson linorder_not_le real_shrink_lt)
+
+lemma real_shrink_grow:
+  fixes x::real
+  shows "\<bar>x\<bar> < 1 \<Longrightarrow> x / (1 - \<bar>x\<bar>) / (1 + \<bar>x / (1 - \<bar>x\<bar>)\<bar>) = x"
+  using real_shrink_Galois by blast
+
+lemma continuous_shrink:
+  "continuous_on UNIV (\<lambda>x::real. x / (1 + \<bar>x\<bar>))"
+  by (intro continuous_intros) auto
+
+lemma strict_mono_shrink:
+  "strict_mono (\<lambda>x::real. x / (1 + \<bar>x\<bar>))"
+  by (simp add: monotoneI real_shrink_lt)
+
+lemma shrink_range: "(\<lambda>x::real. x / (1 + \<bar>x\<bar>)) ` S \<subseteq> {-1<..<1}"
+  by (auto simp: divide_simps)
+
+text \<open>Note: connected sets of real numbers are the same thing as intervals\<close>
+lemma connected_shrink:
+  fixes S :: "real set"
+  shows "connected ((\<lambda>x. x / (1 + \<bar>x\<bar>)) ` S) \<longleftrightarrow> connected S"  (is "?lhs = ?rhs")
+proof 
+  assume "?lhs"
+  then have "connected ((\<lambda>x. x / (1 - \<bar>x\<bar>)) ` (\<lambda>x. x / (1 + \<bar>x\<bar>)) ` S)"
+    by (metis continuous_on_real_grow shrink_range connected_continuous_image 
+               continuous_on_subset)
+  then show "?rhs"
+    using real_grow_shrink by (force simp add: image_comp)
+next
+  assume ?rhs
+  then show ?lhs
+    using connected_continuous_image 
+    by (metis continuous_on_subset continuous_shrink subset_UNIV)
+qed
+
 end
\ No newline at end of file
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Tue May 16 23:41:20 2023 +0200
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Wed May 17 09:00:04 2023 +0200
@@ -437,6 +437,9 @@
   by (meson ball_subset_cball interior_subset mem_interior open_contains_cball open_interior
       subset_trans)
 
+lemma ball_iff_cball: "(\<exists>r>0. ball x r \<subseteq> U) \<longleftrightarrow> (\<exists>r>0. cball x r \<subseteq> U)"
+  by (meson mem_interior mem_interior_cball)
+
 
 subsection \<open>Frontier\<close>
 
--- a/src/HOL/Analysis/Locally.thy	Tue May 16 23:41:20 2023 +0200
+++ b/src/HOL/Analysis/Locally.thy	Wed May 17 09:00:04 2023 +0200
@@ -2,7 +2,7 @@
 
 theory Locally
   imports
-    Path_Connected Function_Topology
+    Path_Connected Function_Topology Sum_Topology
 begin
 
 subsection\<open>Neighbourhood Bases\<close>
@@ -448,4 +448,525 @@
     using False by blast
 qed
 
+lemma locally_path_connected_is_realinterval:
+  assumes "is_interval S"
+  shows "locally_path_connected_space(subtopology euclideanreal S)"
+  unfolding locally_path_connected_space_def
+proof (clarsimp simp add: neighbourhood_base_of openin_subtopology_alt)
+  fix a U
+  assume "a \<in> S" and "a \<in> U" and "open U"
+  then obtain r where "r > 0" and r: "ball a r \<subseteq> U"
+    by (metis open_contains_ball_eq)
+  show "\<exists>W. open W \<and> (\<exists>V. path_connectedin (top_of_set S) V \<and> a \<in> W \<and> S \<inter> W \<subseteq> V \<and> V \<subseteq> S \<and> V \<subseteq> U)"
+  proof (intro exI conjI)
+    show "path_connectedin (top_of_set S) (S \<inter> ball a r)"
+      by (simp add: assms is_interval_Int is_interval_ball_real is_interval_path_connected path_connectedin_subtopology)
+    show "a \<in> ball a r"
+      by (simp add: \<open>0 < r\<close>)
+  qed (use \<open>0 < r\<close> r in auto)
+qed
+
+lemma locally_path_connected_real_interval:
+ "locally_path_connected_space (subtopology euclideanreal{a..b})"
+  "locally_path_connected_space (subtopology euclideanreal{a<..<b})"
+  using locally_path_connected_is_realinterval
+  by (auto simp add: is_interval_1)
+
+lemma locally_path_connected_space_prod_topology:
+   "locally_path_connected_space (prod_topology X Y) \<longleftrightarrow>
+      topspace (prod_topology X Y) = {} \<or>
+      locally_path_connected_space X \<and> locally_path_connected_space Y" (is "?lhs=?rhs")
+proof (cases "topspace(prod_topology X Y) = {}")
+  case True
+  then show ?thesis
+    by (metis equals0D locally_path_connected_space_def neighbourhood_base_of_def)
+next
+  case False
+  then have ne: "topspace X \<noteq> {}" "topspace Y \<noteq> {}"
+    by simp_all
+  show ?thesis
+  proof
+    assume ?lhs then show ?rhs
+      by (metis ne locally_path_connected_space_retraction_map_image retraction_map_fst retraction_map_snd)
+  next
+    assume ?rhs
+    with False have X: "locally_path_connected_space X" and Y: "locally_path_connected_space Y"
+      by auto
+    show ?lhs
+      unfolding locally_path_connected_space_def neighbourhood_base_of
+    proof clarify
+      fix UV x y
+      assume UV: "openin (prod_topology X Y) UV" and "(x,y) \<in> UV"
+      obtain A B where W12: "openin X A \<and> openin Y B \<and> x \<in> A \<and> y \<in> B \<and> A \<times> B \<subseteq> UV"
+        using X Y by (metis UV \<open>(x,y) \<in> UV\<close> openin_prod_topology_alt)
+      then obtain C D K L
+        where "openin X C" "path_connectedin X K" "x \<in> C" "C \<subseteq> K" "K \<subseteq> A"
+          "openin Y D" "path_connectedin Y L" "y \<in> D" "D \<subseteq> L" "L \<subseteq> B"
+        by (metis X Y locally_path_connected_space)
+      with W12 \<open>openin X C\<close> \<open>openin Y D\<close>
+      show "\<exists>U V. openin (prod_topology X Y) U \<and> path_connectedin (prod_topology X Y) V \<and> (x, y) \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> UV"
+        apply (rule_tac x="C \<times> D" in exI)
+        apply (rule_tac x="K \<times> L" in exI)
+        apply (auto simp: openin_prod_Times_iff path_connectedin_Times)
+        done
+    qed
+  qed
+qed
+
+lemma locally_path_connected_space_sum_topology:
+   "locally_path_connected_space(sum_topology X I) \<longleftrightarrow>
+    (\<forall>i \<in> I. locally_path_connected_space (X i))" (is "?lhs=?rhs")
+proof
+  assume ?lhs then show ?rhs
+    by (smt (verit) homeomorphic_locally_path_connected_space locally_path_connected_space_open_subset topological_property_of_sum_component)
+next
+  assume R: ?rhs
+  show ?lhs
+  proof (clarsimp simp add: locally_path_connected_space_def neighbourhood_base_of forall_openin_sum_topology imp_conjL)
+    fix W i x
+    assume ope: "\<forall>i\<in>I. openin (X i) (W i)" 
+      and "i \<in> I" and "x \<in> W i"
+    then obtain U V where U: "openin (X i) U" and V: "path_connectedin (X i) V" 
+           and "x \<in> U" "U \<subseteq> V" "V \<subseteq> W i"
+      by (metis R \<open>i \<in> I\<close> \<open>x \<in> W i\<close> locally_path_connected_space)
+    show "\<exists>U. openin (sum_topology X I) U \<and> (\<exists>V. path_connectedin (sum_topology X I) V \<and> (i, x) \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> Sigma I W)"
+    proof (intro exI conjI)
+      show "openin (sum_topology X I) (Pair i ` U)"
+        by (meson U \<open>i \<in> I\<close> open_map_component_injection open_map_def)
+      show "path_connectedin (sum_topology X I) (Pair i ` V)"
+        by (meson V \<open>i \<in> I\<close> continuous_map_component_injection path_connectedin_continuous_map_image)
+      show "Pair i ` V \<subseteq> Sigma I W"
+        using \<open>V \<subseteq> W i\<close> \<open>i \<in> I\<close> by force
+    qed (use \<open>x \<in> U\<close> \<open>U \<subseteq> V\<close> in auto)
+  qed
+qed
+
+
+subsection\<open>Locally connected spaces\<close>
+
+definition weakly_locally_connected_at 
+  where "weakly_locally_connected_at x X \<equiv> neighbourhood_base_at x (connectedin X) X"
+
+definition locally_connected_at 
+  where "locally_connected_at x X \<equiv>
+           neighbourhood_base_at x (\<lambda>U. openin X U \<and> connectedin X U ) X"
+
+definition locally_connected_space 
+  where "locally_connected_space X \<equiv> neighbourhood_base_of (connectedin X) X"
+
+
+lemma locally_connected_A: "(\<forall>U x. openin X U \<and> x \<in> U
+              \<longrightarrow> openin X (connected_component_of_set (subtopology X U) x))
+       \<Longrightarrow> neighbourhood_base_of (\<lambda>U. openin X U \<and> connectedin X U) X"
+  by (smt (verit, best) connected_component_of_refl connectedin_connected_component_of connectedin_subtopology mem_Collect_eq neighbourhood_base_of openin_subset topspace_subtopology_subset)
+
+lemma locally_connected_B: "locally_connected_space X \<Longrightarrow> 
+          (\<forall>U x. openin X U \<and> x \<in> U \<longrightarrow> openin X (connected_component_of_set (subtopology X U) x))"
+  unfolding locally_connected_space_def neighbourhood_base_of
+  apply (erule all_forward)
+  apply clarify
+  apply (subst openin_subopen)
+  by (smt (verit, ccfv_threshold) Ball_Collect connected_component_of_def connected_component_of_equiv connectedin_subtopology in_mono mem_Collect_eq)
+
+lemma locally_connected_C: "neighbourhood_base_of (\<lambda>U. openin X U \<and> connectedin X U) X \<Longrightarrow> locally_connected_space X"
+  using locally_connected_space_def neighbourhood_base_of_mono by auto
+
+
+lemma locally_connected_space_alt: 
+  "locally_connected_space X \<longleftrightarrow> neighbourhood_base_of (\<lambda>U. openin X U \<and> connectedin X U) X"
+  using locally_connected_A locally_connected_B locally_connected_C by blast
+
+lemma locally_connected_space_eq_open_connected_component_of:
+  "locally_connected_space X \<longleftrightarrow>
+        (\<forall>U x. openin X U \<and> x \<in> U
+              \<longrightarrow> openin X (connected_component_of_set (subtopology X U) x))"
+  by (meson locally_connected_A locally_connected_B locally_connected_C)
+
+lemma locally_connected_space:
+   "locally_connected_space X \<longleftrightarrow>
+     (\<forall>V x. openin X V \<and> x \<in> V \<longrightarrow> (\<exists>U. openin X U \<and> connectedin X U \<and> x \<in> U \<and> U \<subseteq> V))"
+  by (simp add: locally_connected_space_alt open_neighbourhood_base_of)
+
+lemma locally_path_connected_imp_locally_connected_space:
+   "locally_path_connected_space X \<Longrightarrow> locally_connected_space X"
+  by (simp add: locally_connected_space_def locally_path_connected_space_def neighbourhood_base_of_mono path_connectedin_imp_connectedin)
+
+lemma locally_connected_space_open_connected_components:
+  "locally_connected_space X \<longleftrightarrow>
+   (\<forall>U C. openin X U \<and> C \<in> connected_components_of(subtopology X U) \<longrightarrow> openin X C)"
+  apply (simp add: locally_connected_space_eq_open_connected_component_of connected_components_of_def)
+  by (smt (verit) imageE image_eqI inf.orderE inf_commute openin_subset)
+
+lemma openin_connected_component_of_locally_connected_space:
+   "locally_connected_space X \<Longrightarrow> openin X (connected_component_of_set X x)"
+  by (metis connected_component_of_eq_empty locally_connected_space_eq_open_connected_component_of openin_empty openin_topspace subtopology_topspace)
+
+lemma openin_connected_components_of_locally_connected_space:
+   "\<lbrakk>locally_connected_space X; C \<in> connected_components_of X\<rbrakk> \<Longrightarrow> openin X C"
+  by (metis locally_connected_space_open_connected_components openin_topspace subtopology_topspace)
+
+lemma weakly_locally_connected_at:
+   "weakly_locally_connected_at x X \<longleftrightarrow>
+    (\<forall>V. openin X V \<and> x \<in> V
+       \<longrightarrow> (\<exists>U. openin X U \<and> x \<in> U \<and> U \<subseteq> V \<and>
+                (\<forall>y \<in> U. \<exists>C. connectedin X C \<and> C \<subseteq> V \<and> x \<in> C \<and> y \<in> C)))" (is "?lhs=?rhs")
+proof
+  assume ?lhs then show ?rhs
+    unfolding neighbourhood_base_at_def weakly_locally_connected_at_def
+    by (meson subsetD subset_trans)
+next
+  assume R: ?rhs
+  show ?lhs
+    unfolding neighbourhood_base_at_def weakly_locally_connected_at_def
+  proof clarify
+    fix V
+    assume "openin X V" and "x \<in> V"
+    then obtain U where "openin X U" "x \<in> U" "U \<subseteq> V" 
+                  and U: "\<forall>y\<in>U. \<exists>C. connectedin X C \<and> C \<subseteq> V \<and> x \<in> C \<and> y \<in> C"
+      using R by force
+    show "\<exists>A B. openin X A \<and> connectedin X B \<and> x \<in> A \<and> A \<subseteq> B \<and> B \<subseteq> V"
+    proof (intro conjI exI)
+      show "connectedin X (connected_component_of_set (subtopology X V) x)"
+        by (meson connectedin_connected_component_of connectedin_subtopology)
+      show "U \<subseteq> connected_component_of_set (subtopology X V) x"
+        using connected_component_of_maximal U
+        by (simp add: connected_component_of_def connectedin_subtopology subsetI)
+      show "connected_component_of_set (subtopology X V) x \<subseteq> V"
+        using connected_component_of_subset_topspace by fastforce
+    qed (auto simp: \<open>x \<in> U\<close> \<open>openin X U\<close>)
+  qed
+qed
+
+lemma locally_connected_space_iff_weak:
+  "locally_connected_space X \<longleftrightarrow> (\<forall>x \<in> topspace X. weakly_locally_connected_at x X)"
+  by (simp add: locally_connected_space_def neighbourhood_base_of_def weakly_locally_connected_at_def)
+
+lemma locally_connected_space_im_kleinen:
+   "locally_connected_space X \<longleftrightarrow>
+    (\<forall>V x. openin X V \<and> x \<in> V
+          \<longrightarrow> (\<exists>U. openin X U \<and> x \<in> U \<and> U \<subseteq> V \<and>
+                    (\<forall>y \<in> U. \<exists>C. connectedin X C \<and> C \<subseteq> V \<and> x \<in> C \<and> y \<in> C)))"
+  unfolding locally_connected_space_iff_weak weakly_locally_connected_at
+  using openin_subset subsetD by fastforce
+
+lemma locally_connected_space_open_subset:
+   "\<lbrakk>locally_connected_space X; openin X S\<rbrakk> \<Longrightarrow> locally_connected_space (subtopology X S)"
+  apply (simp add: locally_connected_space_def)
+  by (smt (verit, ccfv_threshold) connectedin_subtopology neighbourhood_base_of openin_open_subtopology subset_trans)
+
+lemma locally_connected_space_quotient_map_image:
+  assumes X: "locally_connected_space X" and f: "quotient_map X Y f"
+  shows "locally_connected_space Y"
+  unfolding locally_connected_space_open_connected_components
+proof clarify
+  fix V C
+  assume "openin Y V" and C: "C \<in> connected_components_of (subtopology Y V)"
+  then have "C \<subseteq> topspace Y"
+    using connected_components_of_subset by force
+  have ope1: "openin X {a \<in> topspace X. f a \<in> V}"
+    using \<open>openin Y V\<close> f openin_continuous_map_preimage quotient_imp_continuous_map by blast
+  define Vf where "Vf \<equiv> {z \<in> topspace X. f z \<in> V}"
+  have "openin X {x \<in> topspace X. f x \<in> C}"
+  proof (clarsimp simp: openin_subopen [where S = "{x \<in> topspace X. f x \<in> C}"])
+    fix x
+    assume "x \<in> topspace X" and "f x \<in> C"
+    show "\<exists>T. openin X T \<and> x \<in> T \<and> T \<subseteq> {x \<in> topspace X. f x \<in> C}"
+    proof (intro exI conjI)
+      show "openin X (connected_component_of_set (subtopology X Vf) x)"
+        by (metis Vf_def X connected_component_of_eq_empty locally_connected_B ope1 openin_empty
+                  openin_subset topspace_subtopology_subset)
+      show x_in_conn: "x \<in> connected_component_of_set (subtopology X Vf) x"
+        using C Vf_def \<open>f x \<in> C\<close> \<open>x \<in> topspace X\<close> connected_component_of_refl connected_components_of_subset by fastforce
+      have "connected_component_of_set (subtopology X Vf) x \<subseteq> topspace X \<inter> Vf"
+        using connected_component_of_subset_topspace by fastforce
+      moreover
+      have "f ` connected_component_of_set (subtopology X Vf) x \<subseteq> C"
+      proof (rule connected_components_of_maximal [where X = "subtopology Y V"])
+        show "C \<in> connected_components_of (subtopology Y V)"
+          by (simp add: C)
+        have \<section>: "quotient_map (subtopology X Vf) (subtopology Y V) f"
+          by (simp add: Vf_def \<open>openin Y V\<close> f quotient_map_restriction)
+        then show "connectedin (subtopology Y V) (f ` connected_component_of_set (subtopology X Vf) x)"
+          by (metis connectedin_connected_component_of connectedin_continuous_map_image quotient_imp_continuous_map)
+        show "\<not> disjnt C (f ` connected_component_of_set (subtopology X Vf) x)"
+          using \<open>f x \<in> C\<close> x_in_conn by (auto simp: disjnt_iff)
+      qed
+      ultimately
+      show "connected_component_of_set (subtopology X Vf) x \<subseteq> {x \<in> topspace X. f x \<in> C}"
+        by blast
+    qed
+  qed
+  then show "openin Y C"
+    using \<open>C \<subseteq> topspace Y\<close> f quotient_map_def by fastforce
+qed
+
+
+lemma locally_connected_space_retraction_map_image:
+   "\<lbrakk>retraction_map X Y r; locally_connected_space X\<rbrakk>
+        \<Longrightarrow> locally_connected_space Y"
+  using locally_connected_space_quotient_map_image retraction_imp_quotient_map by blast
+
+lemma homeomorphic_locally_connected_space:
+   "X homeomorphic_space Y \<Longrightarrow> locally_connected_space X \<longleftrightarrow> locally_connected_space Y"
+  by (meson homeomorphic_map_def homeomorphic_space homeomorphic_space_sym locally_connected_space_quotient_map_image)
+
+lemma locally_connected_space_euclideanreal: "locally_connected_space euclideanreal"
+  by (simp add: locally_path_connected_imp_locally_connected_space locally_path_connected_space_euclideanreal)
+
+lemma locally_connected_is_realinterval:
+   "is_interval S \<Longrightarrow> locally_connected_space(subtopology euclideanreal S)"
+  by (simp add: locally_path_connected_imp_locally_connected_space locally_path_connected_is_realinterval)
+
+lemma locally_connected_real_interval:
+    "locally_connected_space (subtopology euclideanreal{a..b})"
+    "locally_connected_space (subtopology euclideanreal{a<..<b})"
+  using connected_Icc is_interval_connected_1 locally_connected_is_realinterval by auto
+
+lemma locally_connected_space_discrete_topology:
+   "locally_connected_space (discrete_topology U)"
+  by (simp add: locally_path_connected_imp_locally_connected_space locally_path_connected_space_discrete_topology)
+
+lemma locally_path_connected_imp_locally_connected_at:
+   "locally_path_connected_at x X \<Longrightarrow> locally_connected_at x X"
+  by (simp add: locally_connected_at_def locally_path_connected_at_def neighbourhood_base_at_mono path_connectedin_imp_connectedin)
+
+lemma weakly_locally_path_connected_imp_weakly_locally_connected_at:
+   "weakly_locally_path_connected_at x X
+             \<Longrightarrow> weakly_locally_connected_at x X"
+  by (simp add: neighbourhood_base_at_mono path_connectedin_imp_connectedin weakly_locally_connected_at_def weakly_locally_path_connected_at_def)
+
+
+lemma interior_of_locally_connected_subspace_component:
+  assumes X: "locally_connected_space X"
+    and C: "C \<in> connected_components_of (subtopology X S)"
+  shows "X interior_of C = C \<inter> X interior_of S"
+proof -
+  obtain Csub: "C \<subseteq> topspace X" "C \<subseteq> S"
+    by (meson C connectedin_connected_components_of connectedin_subset_topspace connectedin_subtopology)
+  show ?thesis
+  proof
+    show "X interior_of C \<subseteq> C \<inter> X interior_of S"
+      by (simp add: Csub interior_of_mono interior_of_subset)
+    have eq: "X interior_of S = \<Union> (connected_components_of (subtopology X (X interior_of S)))"
+      by (metis Union_connected_components_of interior_of_subset_topspace topspace_subtopology_subset)
+    moreover have "C \<inter> D \<subseteq> X interior_of C"
+      if "D \<in> connected_components_of (subtopology X (X interior_of S))" for D
+    proof (cases "C \<inter> D = {}")
+      case False
+      have "D \<subseteq> X interior_of C"
+      proof (rule interior_of_maximal)
+        have "connectedin (subtopology X S) D"
+          by (meson connectedin_connected_components_of connectedin_subtopology interior_of_subset subset_trans that)
+        then show "D \<subseteq> C"
+          by (meson C False connected_components_of_maximal disjnt_def)
+        show "openin X D"
+          using X locally_connected_space_open_connected_components openin_interior_of that by blast
+      qed
+      then show ?thesis 
+        by blast
+    qed auto
+    ultimately show "C \<inter> X interior_of S \<subseteq> X interior_of C"
+      by blast
+  qed
+qed
+
+
+lemma frontier_of_locally_connected_subspace_component:
+  assumes X: "locally_connected_space X" and "closedin X S" 
+    and C: "C \<in> connected_components_of (subtopology X S)"
+  shows "X frontier_of C = C \<inter> X frontier_of S"
+proof -
+  obtain Csub: "C \<subseteq> topspace X" "C \<subseteq> S"
+    by (meson C connectedin_connected_components_of connectedin_subset_topspace connectedin_subtopology)
+  then have "X closure_of C - X interior_of C = C \<inter> X closure_of S - C \<inter> X interior_of S"
+    using assms
+    apply (simp add: closure_of_closedin flip: interior_of_locally_connected_subspace_component)
+    by (metis closedin_connected_components_of closedin_trans_full closure_of_eq inf.orderE)
+  then show ?thesis
+    by (simp add: Diff_Int_distrib frontier_of_def)
+qed
+
+(*Similar proof to locally_connected_space_prod_topology*)
+lemma locally_connected_space_prod_topology:
+   "locally_connected_space (prod_topology X Y) \<longleftrightarrow>
+      topspace (prod_topology X Y) = {} \<or>
+      locally_connected_space X \<and> locally_connected_space Y" (is "?lhs=?rhs")
+proof (cases "topspace(prod_topology X Y) = {}")
+  case True
+  then show ?thesis
+    using locally_connected_space_iff_weak by force
+next
+  case False
+  then have ne: "topspace X \<noteq> {}" "topspace Y \<noteq> {}"
+    by simp_all
+  show ?thesis
+  proof
+    assume ?lhs then show ?rhs
+      by (metis locally_connected_space_quotient_map_image ne quotient_map_fst quotient_map_snd)
+  next
+    assume ?rhs
+    with False have X: "locally_connected_space X" and Y: "locally_connected_space Y"
+      by auto
+    show ?lhs
+      unfolding locally_connected_space_def neighbourhood_base_of
+    proof clarify
+      fix UV x y
+      assume UV: "openin (prod_topology X Y) UV" and "(x,y) \<in> UV"
+
+     obtain A B where W12: "openin X A \<and> openin Y B \<and> x \<in> A \<and> y \<in> B \<and> A \<times> B \<subseteq> UV"
+        using X Y by (metis UV \<open>(x,y) \<in> UV\<close> openin_prod_topology_alt)
+      then obtain C D K L
+        where "openin X C" "connectedin X K" "x \<in> C" "C \<subseteq> K" "K \<subseteq> A"
+          "openin Y D" "connectedin Y L" "y \<in> D" "D \<subseteq> L" "L \<subseteq> B"
+        by (metis X Y locally_connected_space)
+      with W12 \<open>openin X C\<close> \<open>openin Y D\<close>
+      show "\<exists>U V. openin (prod_topology X Y) U \<and> connectedin (prod_topology X Y) V \<and> (x, y) \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> UV"
+        apply (rule_tac x="C \<times> D" in exI)
+        apply (rule_tac x="K \<times> L" in exI)
+        apply (auto simp: openin_prod_Times_iff connectedin_Times)
+        done
+    qed
+  qed
+qed
+
+(*Same proof as locally_path_connected_space_product_topology*)
+lemma locally_connected_space_product_topology:
+   "locally_connected_space(product_topology X I) \<longleftrightarrow>
+        topspace(product_topology X I) = {} \<or>
+        finite {i. i \<in> I \<and> ~connected_space(X i)} \<and>
+        (\<forall>i \<in> I. locally_connected_space(X i))"
+    (is "?lhs \<longleftrightarrow> ?empty \<or> ?rhs")
+proof (cases ?empty)
+  case True
+  then show ?thesis
+    by (simp add: locally_connected_space_def neighbourhood_base_of openin_closedin_eq)
+next
+  case False
+  then obtain z where z: "z \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
+    by auto
+  have ?rhs if L: ?lhs
+  proof -
+    obtain U C where U: "openin (product_topology X I) U"
+      and V: "connectedin (product_topology X I) C"
+      and "z \<in> U" "U \<subseteq> C" and Csub: "C \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
+      using L apply (clarsimp simp add: locally_connected_space_def neighbourhood_base_of)
+      by (metis openin_topspace topspace_product_topology z)
+    then obtain V where finV: "finite {i \<in> I. V i \<noteq> topspace (X i)}"
+      and XV: "\<And>i. i\<in>I \<Longrightarrow> openin (X i) (V i)" and "z \<in> Pi\<^sub>E I V" and subU: "Pi\<^sub>E I V \<subseteq> U"
+      by (force simp: openin_product_topology_alt)
+    show ?thesis
+    proof (intro conjI ballI)
+      have "connected_space (X i)" if "i \<in> I" "V i = topspace (X i)" for i
+      proof -
+        have pc: "connectedin (X i) ((\<lambda>x. x i) ` C)"
+          apply (rule connectedin_continuous_map_image [OF _ V])
+          by (simp add: continuous_map_product_projection \<open>i \<in> I\<close>)
+        moreover have "((\<lambda>x. x i) ` C) = topspace (X i)"
+        proof
+          show "(\<lambda>x. x i) ` C \<subseteq> topspace (X i)"
+            by (simp add: pc connectedin_subset_topspace)
+          have "V i \<subseteq> (\<lambda>x. x i) ` (\<Pi>\<^sub>E i\<in>I. V i)"
+            by (metis \<open>z \<in> Pi\<^sub>E I V\<close> empty_iff image_projection_PiE order_refl that(1))
+          also have "\<dots> \<subseteq> (\<lambda>x. x i) ` U"
+            using subU by blast
+          finally show "topspace (X i) \<subseteq> (\<lambda>x. x i) ` C"
+            using \<open>U \<subseteq> C\<close> that by blast
+        qed
+        ultimately show ?thesis
+          by (simp add: connectedin_topspace)
+      qed
+      then have "{i \<in> I. \<not> connected_space (X i)} \<subseteq> {i \<in> I. V i \<noteq> topspace (X i)}"
+        by blast
+      with finV show "finite {i \<in> I. \<not> connected_space (X i)}"
+        using finite_subset by blast
+    next
+      show "locally_connected_space (X i)" if "i \<in> I" for i
+        by (meson False L locally_connected_space_quotient_map_image quotient_map_product_projection that)
+    qed
+  qed
+  moreover have ?lhs if R: ?rhs
+  proof (clarsimp simp add: locally_connected_space_def neighbourhood_base_of)
+    fix F z
+    assume "openin (product_topology X I) F" and "z \<in> F"
+    then obtain W where finW: "finite {i \<in> I. W i \<noteq> topspace (X i)}"
+            and opeW: "\<And>i. i \<in> I \<Longrightarrow> openin (X i) (W i)" and "z \<in> Pi\<^sub>E I W" "Pi\<^sub>E I W \<subseteq> F"
+      by (auto simp: openin_product_topology_alt)
+    have "\<forall>i \<in> I. \<exists>U C. openin (X i) U \<and> connectedin (X i) C \<and> z i \<in> U \<and> U \<subseteq> C \<and> C \<subseteq> W i \<and>
+                        (W i = topspace (X i) \<and>
+                         connected_space (X i) \<longrightarrow> U = topspace (X i) \<and> C = topspace (X i))"
+          (is "\<forall>i \<in> I. ?\<Phi> i")
+    proof
+      fix i assume "i \<in> I"
+      have "locally_connected_space (X i)"
+        by (simp add: R \<open>i \<in> I\<close>)
+      moreover have "openin (X i) (W i) " "z i \<in> W i"
+        using \<open>z \<in> Pi\<^sub>E I W\<close> opeW \<open>i \<in> I\<close> by auto
+      ultimately obtain U C where UC: "openin (X i) U" "connectedin (X i) C" "z i \<in> U" "U \<subseteq> C" "C \<subseteq> W i"
+        using \<open>i \<in> I\<close> by (force simp: locally_connected_space_def neighbourhood_base_of)
+      show "?\<Phi> i"
+      proof (cases "W i = topspace (X i) \<and> connected_space(X i)")
+        case True
+        then show ?thesis
+          using \<open>z i \<in> W i\<close> connectedin_topspace by blast
+      next
+        case False
+        then show ?thesis
+          by (meson UC)
+      qed
+    qed
+    then obtain U C where
+      *: "\<And>i. i \<in> I \<Longrightarrow> openin (X i) (U i) \<and> connectedin (X i) (C i) \<and> z i \<in> (U i) \<and> (U i) \<subseteq> (C i) \<and> (C i) \<subseteq> W i \<and>
+                        (W i = topspace (X i) \<and> connected_space (X i)
+                         \<longrightarrow> (U i) = topspace (X i) \<and> (C i) = topspace (X i))"
+      by metis
+    let ?A = "{i \<in> I. \<not> connected_space (X i)} \<union> {i \<in> I. W i \<noteq> topspace (X i)}"
+    have "{i \<in> I. U i \<noteq> topspace (X i)} \<subseteq> ?A"
+      by (clarsimp simp add: "*")
+    moreover have "finite ?A"
+      by (simp add: that finW)
+    ultimately have "finite {i \<in> I. U i \<noteq> topspace (X i)}"
+      using finite_subset by auto
+    then have "openin (product_topology X I) (Pi\<^sub>E I U)"
+      using * by (simp add: openin_PiE_gen)
+    then show "\<exists>U. openin (product_topology X I) U \<and>
+            (\<exists>V. connectedin (product_topology X I) V \<and> z \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> F)"
+      apply (rule_tac x="PiE I U" in exI, simp)
+      apply (rule_tac x="PiE I C" in exI)
+      using \<open>z \<in> Pi\<^sub>E I W\<close> \<open>Pi\<^sub>E I W \<subseteq> F\<close> *
+      apply (simp add: connectedin_PiE subset_PiE PiE_iff PiE_mono dual_order.trans)
+      done
+  qed
+  ultimately show ?thesis
+    using False by blast
+qed
+
+lemma locally_connected_space_sum_topology:
+   "locally_connected_space(sum_topology X I) \<longleftrightarrow>
+    (\<forall>i \<in> I. locally_connected_space (X i))" (is "?lhs=?rhs")
+proof
+  assume ?lhs then show ?rhs
+    by (smt (verit) homeomorphic_locally_connected_space locally_connected_space_open_subset topological_property_of_sum_component)
+next
+  assume R: ?rhs
+  show ?lhs
+  proof (clarsimp simp add: locally_connected_space_def neighbourhood_base_of forall_openin_sum_topology imp_conjL)
+    fix W i x
+    assume ope: "\<forall>i\<in>I. openin (X i) (W i)" 
+      and "i \<in> I" and "x \<in> W i"
+    then obtain U V where U: "openin (X i) U" and V: "connectedin (X i) V" 
+           and "x \<in> U" "U \<subseteq> V" "V \<subseteq> W i"
+      by (metis R \<open>i \<in> I\<close> \<open>x \<in> W i\<close> locally_connected_space)
+    show "\<exists>U. openin (sum_topology X I) U \<and> (\<exists>V. connectedin (sum_topology X I) V \<and> (i,x) \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> Sigma I W)"
+    proof (intro exI conjI)
+      show "openin (sum_topology X I) (Pair i ` U)"
+        by (meson U \<open>i \<in> I\<close> open_map_component_injection open_map_def)
+      show "connectedin (sum_topology X I) (Pair i ` V)"
+        by (meson V \<open>i \<in> I\<close> continuous_map_component_injection connectedin_continuous_map_image)
+      show "Pair i ` V \<subseteq> Sigma I W"
+        using \<open>V \<subseteq> W i\<close> \<open>i \<in> I\<close> by force
+    qed (use \<open>x \<in> U\<close> \<open>U \<subseteq> V\<close> in auto)
+  qed
+qed
+
+
 end
--- a/src/HOL/Analysis/Product_Topology.thy	Tue May 16 23:41:20 2023 +0200
+++ b/src/HOL/Analysis/Product_Topology.thy	Wed May 17 09:00:04 2023 +0200
@@ -576,5 +576,68 @@
     by (metis prod.collapse)
 qed
 
+proposition connected_space_prod_topology:
+   "connected_space(prod_topology X Y) \<longleftrightarrow>
+    topspace(prod_topology X Y) = {} \<or> connected_space X \<and> connected_space Y" (is "?lhs=?rhs")
+proof (cases "topspace(prod_topology X Y) = {}")
+  case True
+  then show ?thesis
+    using connected_space_topspace_empty by blast
+next
+  case False
+  then have nonempty: "topspace X \<noteq> {}" "topspace Y \<noteq> {}"
+    by force+
+  show ?thesis 
+  proof
+    assume ?lhs
+    then show ?rhs
+      by (meson connected_space_quotient_map_image nonempty quotient_map_fst quotient_map_snd)
+  next
+    assume ?rhs
+    then have conX: "connected_space X" and conY: "connected_space Y"
+      using False by blast+
+    have False
+      if "openin (prod_topology X Y) U" and "openin (prod_topology X Y) V"
+        and UV: "topspace X \<times> topspace Y \<subseteq> U \<union> V" "U \<inter> V = {}" 
+        and "U \<noteq> {}" and "V \<noteq> {}"
+      for U V
+    proof -
+      have Usub: "U \<subseteq> topspace X \<times> topspace Y" and Vsub: "V \<subseteq> topspace X \<times> topspace Y"
+        using that by (metis openin_subset topspace_prod_topology)+
+      obtain a b where ab: "(a,b) \<in> U" and a: "a \<in> topspace X" and b: "b \<in> topspace Y"
+        using \<open>U \<noteq> {}\<close> Usub by auto
+      have "\<not> topspace X \<times> topspace Y \<subseteq> U"
+        using Usub Vsub \<open>U \<inter> V = {}\<close> \<open>V \<noteq> {}\<close> by auto
+      then obtain x y where x: "x \<in> topspace X" and y: "y \<in> topspace Y" and "(x,y) \<notin> U"
+        by blast
+      have oX: "openin X {x \<in> topspace X. (x,y) \<in> U}" "openin X {x \<in> topspace X. (x,y) \<in> V}"
+       and oY: "openin Y {y \<in> topspace Y. (a,y) \<in> U}" "openin Y {y \<in> topspace Y. (a,y) \<in> V}"
+        by (force intro: openin_continuous_map_preimage [where Y = "prod_topology X Y"] 
+            simp: that continuous_map_pairwise o_def x y a)+
+      have 1: "topspace Y \<subseteq> {y \<in> topspace Y. (a,y) \<in> U} \<union> {y \<in> topspace Y. (a,y) \<in> V}"
+        using a that(3) by auto
+      have 2: "{y \<in> topspace Y. (a,y) \<in> U} \<inter> {y \<in> topspace Y. (a,y) \<in> V} = {}"
+        using that(4) by auto
+      have 3: "{y \<in> topspace Y. (a,y) \<in> U} \<noteq> {}"
+        using ab b by auto
+      have 4: "{y \<in> topspace Y. (a,y) \<in> V} \<noteq> {}"
+      proof -
+        show ?thesis
+          using connected_spaceD [OF conX oX] UV \<open>(x,y) \<notin> U\<close> a x y
+                disjoint_iff_not_equal by blast
+      qed
+      show ?thesis
+        using connected_spaceD [OF conY oY 1 2 3 4] by auto
+    qed
+    then show ?lhs
+      unfolding connected_space_def topspace_prod_topology by blast 
+  qed
+qed
+
+lemma connectedin_Times:
+   "connectedin (prod_topology X Y) (S \<times> T) \<longleftrightarrow>
+        S = {} \<or> T = {} \<or> connectedin X S \<and> connectedin Y T"
+  by (force simp: connectedin_def subtopology_Times connected_space_prod_topology)
+
 end
 
--- a/src/HOL/Analysis/Starlike.thy	Tue May 16 23:41:20 2023 +0200
+++ b/src/HOL/Analysis/Starlike.thy	Wed May 17 09:00:04 2023 +0200
@@ -882,6 +882,11 @@
     convex_rel_interior_closure[of S] assms
   by auto
 
+lemma open_subset_closure_of_interval:
+  assumes "open U" "is_interval S"
+  shows "U \<subseteq> closure S \<longleftrightarrow> U \<subseteq> interior S"
+  by (metis assms convex_interior_closure is_interval_convex open_subset_interior)
+
 lemma closure_eq_rel_interior_eq:
   fixes S1 S2 :: "'n::euclidean_space set"
   assumes "convex S1"
--- a/src/HOL/Analysis/Sum_Topology.thy	Tue May 16 23:41:20 2023 +0200
+++ b/src/HOL/Analysis/Sum_Topology.thy	Wed May 17 09:00:04 2023 +0200
@@ -143,4 +143,20 @@
   by (metis injective_open_imp_embedding_map continuous_map_component_injection
             open_map_component_injection inj_onI prod.inject)
 
+lemma topological_property_of_sum_component:
+  assumes major: "P (sum_topology X I)"
+    and minor: "\<And>X S. \<lbrakk>P X; closedin X S; openin X S\<rbrakk> \<Longrightarrow> P(subtopology X S)"
+    and PQ:  "\<And>X Y. X homeomorphic_space Y \<Longrightarrow> (P X \<longleftrightarrow> Q Y)"
+  shows "(\<forall>i \<in> I. Q(X i))"
+proof -
+  have "Q(X i)" if "i \<in> I" for i
+  proof -
+    have "P(subtopology (sum_topology X I) (Pair i ` topspace (X i)))"
+      by (meson closed_map_component_injection closed_map_def closedin_topspace major minor open_map_component_injection open_map_def openin_topspace that)
+    then show ?thesis
+      by (metis PQ embedding_map_component_injection embedding_map_imp_homeomorphic_space homeomorphic_space_sym that)
+  qed
+  then show ?thesis by metis
+qed
+
 end
--- a/src/HOL/Statespace/state_space.ML	Tue May 16 23:41:20 2023 +0200
+++ b/src/HOL/Statespace/state_space.ML	Wed May 17 09:00:04 2023 +0200
@@ -36,7 +36,6 @@
        (((string * bool) * (string list * xstring * (bstring * bstring) list)) list *
         (bstring * string) list)) parser
 
-
   val neq_x_y : Proof.context -> term -> term -> thm option
   val distinctNameSolver : Simplifier.solver
   val distinctTree_tac : Proof.context -> int -> tactic
@@ -49,9 +48,7 @@
   val get_comp : Context.generic -> string -> (typ * string) option (* legacy wrapper, eventually replace by primed version *)
   val get_comps : Context.generic -> (typ * string list) Termtab.table
 
-  val get_silent : Context.generic -> bool
-  val set_silent : bool -> Context.generic -> Context.generic
-
+  val silent : bool Config.T
 
   val gen_lookup_tr : Proof.context -> term -> string -> term
   val lookup_swap_tr : Proof.context -> term list -> term
@@ -66,8 +63,7 @@
   val update_tr : Proof.context -> term list -> term
   val update_tr' : Proof.context -> term list -> term
 
-  val trace_name_space_data: Context.generic -> unit
-  val trace_state_space_data: Context.generic -> unit
+  val trace_data: Context.generic -> unit
 end;
 
 structure StateSpace : STATE_SPACE =
@@ -101,29 +97,26 @@
 
 fun insert_tagged_distinct_thms tagged_thm tagged_thms =
  let
-   fun ins t1 [] = [t1] 
+   fun ins t1 [] = [t1]
      | ins (t1 as (names1, _)) ((t2 as (names2, _))::thms) =
          if Ord_List.subset string_ord (names1, names2) then t2::thms
          else if Ord_List.subset string_ord (names2, names1) then ins t1 thms
          else t2 :: ins t1 thms
- in 
+ in
    ins tagged_thm tagged_thms
  end
 
-fun join_tagged_distinct_thms tagged_thms1 tagged_thms2 = 
+fun join_tagged_distinct_thms tagged_thms1 tagged_thms2 =
   tagged_thms1 |> fold insert_tagged_distinct_thms tagged_thms2
 
 fun tag_distinct_thm thm = (comps_of_distinct_thm thm, thm)
 val tag_distinct_thms = map tag_distinct_thm
 
-fun join_distinct_thms thms1 thms2 = 
-  if pointer_eq (thms1, thms2) then thms1 
-  else join_tagged_distinct_thms (tag_distinct_thms thms1) (tag_distinct_thms thms2) 
-       |> map snd
+fun join_distinct_thms (thms1, thms2) =
+  if pointer_eq (thms1, thms2) then thms1
+  else join_tagged_distinct_thms (tag_distinct_thms thms1) (tag_distinct_thms thms2) |> map snd
 
-fun insert_distinct_thm thm thms = join_distinct_thms thms [thm]
-
-val join_distinctthm_tab = Symtab.join (fn name => fn (thms1, thms2) => join_distinct_thms thms1 thms2)
+fun insert_distinct_thm thm thms = join_distinct_thms (thms, [thm])
 
 
 fun join_declinfo_entry name (T1:typ, names1:string list) (T2, names2) =
@@ -131,68 +124,67 @@
     fun typ_info T names = @{make_string} T ^ " "  ^ Pretty.string_of (Pretty.str_list "(" ")" names);
   in
     if T1 = T2 then (T1, distinct (op =) (names1 @ names2))
-    else error ("statespace component '" ^ name ^ "' disagrees on type:\n " ^ 
+    else error ("statespace component '" ^ name ^ "' disagrees on type:\n " ^
        typ_info T1 names1 ^ " vs. "  ^ typ_info T2 names2
-     ) 
+     )
   end
 fun guess_name (Free (x,_)) = x
   | guess_name _ = "unknown"
 
-val join_declinfo = Termtab.join (fn trm => uncurry (join_declinfo_entry (guess_name trm))) 
+val join_declinfo = Termtab.join (fn t => uncurry (join_declinfo_entry (guess_name t)))
 
 
 (*
   A component might appear in *different* statespaces within the same context. However, it must
   be mapped to the same type. Note that this information is currently only properly maintained
   within contexts where all components are actually "fixes" and not arbitrary terms. Moreover, on
-  the theory level the info stays empty. 
+  the theory level the info stays empty.
 
   This means that on the theory level we do not make use of the syntax and the tree-based distinct simprocs.
-  N.B: It might still make sense (from a performance perspective) to overcome this limitation 
+  N.B: It might still make sense (from a performance perspective) to overcome this limitation
   and even use the simprocs when a statespace is interpreted for concrete names like HOL-strings.
-  Once the distinct-theorem is proven by the interpretation the simproc can use the positions in 
-  the tree to derive distinctness of two strings vs. HOL-string comparison. 
+  Once the distinct-theorem is proven by the interpretation the simproc can use the positions in
+  the tree to derive distinctness of two strings vs. HOL-string comparison.
  *)
-type namespace_info =
- {declinfo: (typ * string list) Termtab.table, (* type, names of statespaces of component  *)
-  distinctthm: thm list Symtab.table, (* minimal list of maximal distinctness-assumptions for a component name *)
-  silent: bool
+
+type statespace_info =
+ {args: (string * sort) list, (* type arguments *)
+  parents: (typ list * string * string option list) list,
+             (* type instantiation, state-space name, component renamings *)
+  components: (string * typ) list,
+  types: typ list (* range types of state space *)
  };
 
-structure NameSpaceData = Generic_Data
+structure Data = Generic_Data
 (
-  type T = namespace_info;
-  val empty = {declinfo = Termtab.empty, distinctthm = Symtab.empty, silent = false};
-  fun merge
-    ({declinfo=declinfo1, distinctthm=distinctthm1, silent=silent1},
-      {declinfo=declinfo2, distinctthm=distinctthm2, silent=silent2}) : T =
-    {declinfo = join_declinfo (declinfo1, declinfo2),
-     distinctthm = join_distinctthm_tab (distinctthm1, distinctthm2),
-     silent = silent1 andalso silent2 (* FIXME odd merge *)}
+  type T =
+    (typ * string list) Termtab.table * (*declinfo: type, names of statespaces of component*)
+    thm list Symtab.table * (*distinctthm: minimal list of maximal distinctness-assumptions for a component name*)
+    statespace_info Symtab.table;
+  val empty = (Termtab.empty, Symtab.empty, Symtab.empty);
+  fun merge ((declinfo1, distinctthm1, statespaces1), (declinfo2, distinctthm2, statespaces2)) =
+   (join_declinfo (declinfo1, declinfo2),
+    Symtab.join (K join_distinct_thms) (distinctthm1, distinctthm2),
+    Symtab.merge (K true) (statespaces1, statespaces2));
 );
 
-fun trace_name_space_data context =  
-  tracing ("NameSpaceData: " ^ @{make_string} (NameSpaceData.get context))
+val get_declinfo = #1 o Data.get
+val get_distinctthm = #2 o Data.get
+val get_statespaces = #3 o Data.get
 
-fun make_namespace_data declinfo distinctthm silent =
-     {declinfo=declinfo,distinctthm=distinctthm,silent=silent};
-
+val map_declinfo = Data.map o @{apply 3(1)}
+val map_distinctthm = Data.map o @{apply 3(2)}
+val map_statespaces = Data.map o @{apply 3(3)}
 
-fun update_declinfo (n,v) ctxt =
-  let 
-    val {declinfo,distinctthm,silent} = NameSpaceData.get ctxt;
-    val v = apsnd single v
-  in NameSpaceData.put
-      (make_namespace_data (Termtab.map_default (n,v) (join_declinfo_entry (guess_name n) v) declinfo) distinctthm silent) ctxt
-  end;
+fun trace_data context =
+  tracing ("StateSpace.Data: " ^ @{make_string}
+   {declinfo = get_declinfo context,
+    distinctthm = get_distinctthm context,
+    statespaces = get_statespaces context})
 
-fun set_silent silent ctxt =
-  let val {declinfo,distinctthm,...} = NameSpaceData.get ctxt;
-  in NameSpaceData.put
-      (make_namespace_data declinfo distinctthm silent) ctxt
-  end;
-
-val get_silent = #silent o NameSpaceData.get;
+fun update_declinfo (n,v) = map_declinfo (fn declinfo =>
+  let val vs = apsnd single v
+  in Termtab.map_default (n, vs) (join_declinfo_entry (guess_name n) vs) declinfo end);
 
 fun expression_no_pos (expr, fixes) : Expression.expression =
   (map (fn (name, inst) => ((name, Position.none), inst)) expr, fixes);
@@ -216,52 +208,31 @@
   |> snd
   |> Local_Theory.exit;
 
-type statespace_info =
- {args: (string * sort) list, (* type arguments *)
-  parents: (typ list * string * string option list) list,
-             (* type instantiation, state-space name, component renamings *)
-  components: (string * typ) list,
-  types: typ list (* range types of state space *)
- };
-
-structure StateSpaceData = Generic_Data
-(
-  type T = statespace_info Symtab.table;
-  val empty = Symtab.empty;
-  fun merge data : T = Symtab.merge (K true) data;
-);
+fun is_statespace context name =
+  Symtab.defined (get_statespaces context) (Locale.intern (Context.theory_of context) name)
 
-fun is_statespace context name =
-  Symtab.defined (StateSpaceData.get context) (Locale.intern (Context.theory_of context) name)
-
-fun trace_state_space_data context =  
-  tracing ("StateSpaceData: " ^ @{make_string} (StateSpaceData.get context))
+fun add_statespace name args parents components types =
+  map_statespaces (Symtab.update_new (name, {args=args,parents=parents, components=components,types=types}))
 
-fun add_statespace name args parents components types ctxt =
-     StateSpaceData.put
-      (Symtab.update_new (name, {args=args,parents=parents,
-                                components=components,types=types}) (StateSpaceData.get ctxt))
-      ctxt;
-
-fun get_statespace ctxt name =
-      Symtab.lookup (StateSpaceData.get ctxt) name;
+val get_statespace = Symtab.lookup o get_statespaces
+val the_statespace = the oo get_statespace
 
 
 fun mk_free ctxt name =
   if Variable.is_fixed ctxt name orelse Variable.is_declared ctxt name
   then
-    let 
+    let
       val n' = Variable.intern_fixed ctxt name |> perhaps Long_Name.dest_hidden;
       val free = Free (n', Proof_Context.infer_type ctxt (n', dummyT))
     in SOME (free) end
   else (tracing ("variable not fixed or declared: " ^ name); NONE)
 
 
-fun get_dist_thm ctxt name = Symtab.lookup (#distinctthm (NameSpaceData.get ctxt)) name;
+val get_dist_thm = Symtab.lookup o get_distinctthm;
 
-fun get_dist_thm2 ctxt x y = 
+fun get_dist_thm2 ctxt x y =
  (let
-    val dist_thms = [x, y] |> map (#1 o dest_Free) 
+    val dist_thms = [x, y] |> map (#1 o dest_Free)
       |> map (these o get_dist_thm (Context.Proof ctxt)) |> flat;
 
     fun get_paths dist_thm =
@@ -272,30 +243,31 @@
         val y_path = the (DistinctTreeProver.find_tree y tree);
       in SOME (dist_thm, x_path, y_path) end
       handle Option.Option => NONE
-    
+
     val result = get_first get_paths dist_thms
-  in 
+  in
     result
   end)
-    
-       
-fun get_comp' ctxt name =
-  mk_free (Context.proof_of ctxt) name 
-  |> Option.mapPartial (fn t => 
+
+
+fun get_comp' context name =
+  mk_free (Context.proof_of context) name
+  |> Option.mapPartial (fn t =>
        let
-         val declinfo = #declinfo (NameSpaceData.get ctxt)
-       in 
+         val declinfo = get_declinfo context
+       in
          case Termtab.lookup declinfo t of
-           NONE => (* during syntax phase, types of fixes might not yet be constrained completely *) 
+           NONE => (* during syntax phase, types of fixes might not yet be constrained completely *)
              AList.lookup (fn (x, Free (n,_)) => n = x | _ => false) (Termtab.dest declinfo) name
          | some => some
        end)
 
 (* legacy wrapper *)
 fun get_comp ctxt name =
- get_comp' ctxt name |> Option.map (apsnd (fn ns => if null ns then "" else hd ns)) 
+ get_comp' ctxt name |> Option.map (apsnd (fn ns => if null ns then "" else hd ns))
 
-fun get_comps ctxt = #declinfo (NameSpaceData.get ctxt)
+val get_comps = get_declinfo
+
 
 (*** Tactics ***)
 
@@ -356,9 +328,10 @@
         Context.Theory _ => context
       | Context.Proof ctxt =>
         let
-          val {declinfo,distinctthm=tt,silent} = NameSpaceData.get context;
+          val declinfo = get_declinfo context
+          val tt = get_distinctthm context;
           val all_names = comps_of_distinct_thm thm;
-          fun upd name = Symtab.map_default (name, [thm]) (fn thms => insert_distinct_thm thm thms)
+          fun upd name = Symtab.map_default (name, [thm]) (insert_distinct_thm thm)
 
           val tt' = tt |> fold upd all_names;
           val context' =
@@ -366,7 +339,8 @@
               addsimprocs [distinct_simproc]
               |> Context_Position.restore_visible ctxt
               |> Context.Proof
-              |> NameSpaceData.put {declinfo=declinfo,distinctthm=tt',silent=silent};
+              |> map_declinfo (K declinfo)
+              |> map_distinctthm (K tt');
         in context' end));
 
     val attr = Attrib.internal type_attr;
@@ -406,11 +380,10 @@
 
 fun parent_components thy (Ts, pname, renaming) =
   let
-    val ctxt = Context.Theory thy;
     fun rename [] xs = xs
       | rename (NONE::rs)  (x::xs) = x::rename rs xs
       | rename (SOME r::rs) ((x,T)::xs) = (r,T)::rename rs xs;
-    val {args, parents, components, ...} = the (Symtab.lookup (StateSpaceData.get ctxt) pname);
+    val {args, parents, components, ...} = the_statespace (Context.Theory thy) pname;
     val inst = map fst args ~~ Ts;
     val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst);
     val parent_comps =
@@ -451,8 +424,7 @@
 
     fun interprete_parent_valuetypes (prefix, (Ts, pname, _)) thy =
       let
-        val {args,types,...} =
-             the (Symtab.lookup (StateSpaceData.get (Context.Theory thy)) pname);
+        val {args,types,...} = the_statespace (Context.Theory thy) pname;
         val inst = map fst args ~~ Ts;
         val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst);
         val pars = maps ((fn T => [project_name T,inject_name T]) o subst) types;
@@ -481,7 +453,7 @@
               in Context.proof_map
                   (update_declinfo (Morphism.term phi (Free (n,nT)),v))
               end;
-            val ctxt' = ctxt |> fold upd updates 
+            val ctxt' = ctxt |> fold upd updates
           in ctxt' end;
 
       in Context.mapping I upd_prf ctxt end;
@@ -558,7 +530,7 @@
         val {args,components,...} =
               (case get_statespace (Context.Theory thy) full_pname of
                 SOME r => r
-               | NONE => error ("Undefined statespace " ^ quote pname));
+              | NONE => error ("Undefined statespace " ^ quote pname));
 
 
         val (Ts',env') = fold_map (prep_typ ctxt) Ts env
@@ -650,6 +622,7 @@
 
 (*** parse/print - translations ***)
 
+val silent = Attrib.setup_config_bool \<^binding>\<open>statespace_silent\<close> (K false);
 
 fun gen_lookup_tr ctxt s n =
   (case get_comp' (Context.Proof ctxt) n of
@@ -657,7 +630,7 @@
       Syntax.const \<^const_name>\<open>StateFun.lookup\<close> $
         Syntax.free (project_name T) $ Syntax.free n $ s
   | NONE =>
-      if get_silent (Context.Proof ctxt)
+      if Config.get ctxt silent
       then Syntax.const \<^const_name>\<open>StateFun.lookup\<close> $
         Syntax.const \<^const_syntax>\<open>undefined\<close> $ Syntax.free n $ s
       else raise TERM ("StateSpace.gen_lookup_tr: component " ^ quote n ^ " not defined", []));
@@ -690,7 +663,7 @@
           Syntax.free (pname T) $ Syntax.free (iname T) $
           Syntax.free n $ v $ s
     | NONE =>
-        if get_silent (Context.Proof ctxt) then
+        if Config.get ctxt silent then
           Syntax.const \<^const_name>\<open>StateFun.update\<close> $
             Syntax.const \<^const_syntax>\<open>undefined\<close> $ Syntax.const \<^const_syntax>\<open>undefined\<close> $
             Syntax.free n $ v $ s
--- a/src/HOL/Tools/Lifting/lifting_info.ML	Tue May 16 23:41:20 2023 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML	Wed May 17 09:00:04 2023 +0200
@@ -145,7 +145,7 @@
   let
     fun quot_term_absT ctxt quot_term =
       let
-        val (_, abs, _, _) = (dest_Quotient o HOLogic.dest_Trueprop) quot_term
+        val (_, abs, _, _) = dest_Quotient (HOLogic.dest_Trueprop quot_term)
           handle TERM (_, [t]) => error (Pretty.string_of (Pretty.block
             [Pretty.str "The Quotient map theorem is not in the right form.",
              Pretty.brk 1,
@@ -167,10 +167,11 @@
     val extra_prem_tfrees =
       case subtract (op =) concl_tfrees prems_tfrees of
         [] => []
-      | extras => [Pretty.block ([Pretty.str "Extra type variables in the premises:",
-                                 Pretty.brk 1] @
-                                 ((Pretty.commas o map (Pretty.str o quote)) extras) @
-                                 [Pretty.str "."])]
+      | extras =>
+          [Pretty.block ([Pretty.str "Extra type variables in the premises:",
+           Pretty.brk 1] @
+           Pretty.commas (map (Pretty.str o quote) extras) @
+           [Pretty.str "."])]
     val errs = extra_prem_tfrees
   in
     if null errs then () else error (cat_lines (["Sanity check of the quotient map theorem failed:",""]
@@ -181,13 +182,11 @@
 fun add_quot_map rel_quot_thm context =
   let
     val _ = Context.cases (K ()) (quot_map_thm_sanity_check rel_quot_thm) context
-    val rel_quot_thm_concl = (Logic.strip_imp_concl o Thm.prop_of) rel_quot_thm
-    val (_, abs, _, _) = (dest_Quotient o HOLogic.dest_Trueprop) rel_quot_thm_concl
-    val relatorT_name = (fst o dest_Type o fst o dest_funT o fastype_of) abs
+    val rel_quot_thm_concl = Logic.strip_imp_concl (Thm.prop_of rel_quot_thm)
+    val (_, abs, _, _) = dest_Quotient (HOLogic.dest_Trueprop rel_quot_thm_concl)
+    val relatorT_name = fst (dest_Type (fst (dest_funT (fastype_of abs))))
     val minfo = {rel_quot_thm = Thm.trim_context rel_quot_thm}
-  in
-    Data.map (map_quot_maps (Symtab.update (relatorT_name, minfo))) context
-  end
+  in (Data.map o map_quot_maps) (Symtab.update (relatorT_name, minfo)) context end
 
 val _ =
   Theory.setup
@@ -224,7 +223,7 @@
 fun lookup_quot_thm_quotients ctxt quot_thm =
   let
     val (_, qtyp) = quot_thm_rty_qty quot_thm
-    val qty_full_name = (fst o dest_Type) qtyp
+    val qty_full_name = fst (dest_Type qtyp)
     fun compare_data (data:quotient) = Thm.eq_thm_prop (#quot_thm data, quot_thm)
   in
     case lookup_quotients ctxt qty_full_name of
@@ -234,15 +233,15 @@
 
 fun update_quotients type_name qinfo context =
   let val qinfo' = transform_quotient Morphism.trim_context_morphism qinfo
-  in Data.map (map_quotients (Symtab.update (type_name, qinfo'))) context end
+  in (Data.map o map_quotients) (Symtab.update (type_name, qinfo')) context end
 
 fun delete_quotients quot_thm context =
   let
     val (_, qtyp) = quot_thm_rty_qty quot_thm
-    val qty_full_name = (fst o dest_Type) qtyp
+    val qty_full_name = fst (dest_Type qtyp)
   in
     if is_some (lookup_quot_thm_quotients (Context.proof_of context) quot_thm)
-    then Data.map (map_quotients (Symtab.delete qty_full_name)) context
+    then (Data.map o map_quotients) (Symtab.delete qty_full_name) context
     else context
   end
 
@@ -273,7 +272,7 @@
 fun lookup_restore_data ctxt bundle_name = Symtab.lookup (get_restore_data ctxt) bundle_name
 
 fun update_restore_data bundle_name restore_data context =
-  Data.map (map_restore_data (Symtab.update (bundle_name, restore_data))) context
+  (Data.map o map_restore_data) (Symtab.update (bundle_name, restore_data)) context
 
 fun init_restore_data bundle_name qinfo context =
   update_restore_data bundle_name { quotient = qinfo, transfer_rules = Thm.item_net } context
@@ -299,7 +298,7 @@
   |> map (Thm.transfer' ctxt)
 
 fun add_reflexivity_rule thm =
-  Data.map (map_reflexivity_rules (Item_Net.update (Thm.trim_context thm)))
+  (Data.map o map_reflexivity_rules) (Item_Net.update (Thm.trim_context thm))
 
 val add_reflexivity_rule_attribute = Thm.declaration_attribute add_reflexivity_rule
 
@@ -371,11 +370,11 @@
 
     fun find_eq_rule thm =
       let
-        val concl_rhs = (hd o get_args 1 o HOLogic.dest_Trueprop o Thm.concl_of) thm
+        val concl_rhs = hd (get_args 1 (HOLogic.dest_Trueprop (Thm.concl_of thm)))
         val rules = Transfer.retrieve_relator_eq ctxt concl_rhs
       in
         find_first (fn th => Pattern.matches thy (concl_rhs,
-          (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.concl_of) th)) rules
+          fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.concl_of th))))) rules
       end
 
     val eq_rule = find_eq_rule mono_rule;
@@ -391,8 +390,9 @@
 fun add_mono_rule mono_rule context =
   let
     val pol_mono_rule = introduce_polarities mono_rule
-    val mono_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o
-      dest_Const o head_of o HOLogic.dest_Trueprop o Thm.concl_of) pol_mono_rule
+    val mono_ruleT_name =
+      fst (dest_Type (fst (relation_types (fst (relation_types
+        (snd (dest_Const (head_of (HOLogic.dest_Trueprop (Thm.concl_of pol_mono_rule))))))))))
   in
     if Symtab.defined (get_relator_distr_data' context) mono_ruleT_name
     then
@@ -402,11 +402,14 @@
     else
       let
         val neg_mono_rule = negate_mono_rule pol_mono_rule
-        val relator_distr_data = {pos_mono_rule = pol_mono_rule, neg_mono_rule = neg_mono_rule,
-          pos_distr_rules = [], neg_distr_rules = []}
+        val relator_distr_data =
+         {pos_mono_rule = Thm.trim_context pol_mono_rule,
+          neg_mono_rule = Thm.trim_context neg_mono_rule,
+          pos_distr_rules = [],
+          neg_distr_rules = []}
       in
         context
-        |> Data.map (map_relator_distr_data (Symtab.update (mono_ruleT_name, relator_distr_data)))
+        |> (Data.map o map_relator_distr_data) (Symtab.update (mono_ruleT_name, relator_distr_data))
         |> add_reflexivity_rules mono_rule
       end
   end;
@@ -414,12 +417,13 @@
 local
   fun add_distr_rule update_entry distr_rule context =
     let
-      val distr_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o
-        dest_Const o head_of o HOLogic.dest_Trueprop o Thm.concl_of) distr_rule
+      val distr_ruleT_name =
+        fst (dest_Type (fst (relation_types (fst (relation_types
+          (snd (dest_Const (head_of (HOLogic.dest_Trueprop (Thm.concl_of distr_rule))))))))))
     in
       if Symtab.defined (get_relator_distr_data' context) distr_ruleT_name then
-        Data.map (map_relator_distr_data (Symtab.map_entry distr_ruleT_name (update_entry distr_rule)))
-          context
+        (Data.map o map_relator_distr_data)
+          (Symtab.map_entry distr_ruleT_name (update_entry distr_rule)) context
       else error "The monotonicity rule is not defined."
     end
 
@@ -430,21 +434,25 @@
 in
   fun add_pos_distr_rule distr_rule context =
     let
-      val distr_rule = Conv.fconv_rule (rewrite_concl_conv @{thm POS_def}) distr_rule
+      val distr_rule' = Conv.fconv_rule (rewrite_concl_conv @{thm POS_def}) distr_rule
       fun update_entry distr_rule data =
-        map_pos_distr_rules (cons (@{thm POS_trans} OF [distr_rule, #pos_mono_rule data])) data
+        data |> (map_pos_distr_rules o cons)
+          (Thm.trim_context (@{thm POS_trans} OF
+            [distr_rule, Thm.transfer'' context (#pos_mono_rule data)]))
     in
-      add_distr_rule update_entry distr_rule context
+      add_distr_rule update_entry distr_rule' context
     end
     handle THM _ => error "Combining of the distr. rule and the monotonicity rule together has failed."
 
   fun add_neg_distr_rule distr_rule context =
     let
-      val distr_rule = Conv.fconv_rule (rewrite_concl_conv @{thm NEG_def}) distr_rule
+      val distr_rule' = Conv.fconv_rule (rewrite_concl_conv @{thm NEG_def}) distr_rule
       fun update_entry distr_rule data =
-        map_neg_distr_rules (cons (@{thm NEG_trans} OF [distr_rule, #neg_mono_rule data])) data
+        data |> (map_neg_distr_rules o cons)
+          (Thm.trim_context (@{thm NEG_trans} OF
+            [distr_rule, Thm.transfer'' context (#neg_mono_rule data)]))
     in
-      add_distr_rule update_entry distr_rule context
+      add_distr_rule update_entry distr_rule' context
     end
     handle THM _ => error "Combining of the distr. rule and the monotonicity rule together has failed."
 end
@@ -467,7 +475,7 @@
   fun sanity_check rule =
     let
       val assms = map (perhaps (try HOLogic.dest_Trueprop)) (Thm.prems_of rule)
-      val concl = (perhaps (try HOLogic.dest_Trueprop)) (Thm.concl_of rule);
+      val concl = perhaps (try HOLogic.dest_Trueprop) (Thm.concl_of rule);
       val (lhs, rhs) =
         (case concl of
           Const (\<^const_name>\<open>less_eq\<close>, _) $ (lhs as Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) $ rhs =>
@@ -502,7 +510,7 @@
   fun add_distr_rule distr_rule context =
     let
       val _ = sanity_check distr_rule
-      val concl = (perhaps (try HOLogic.dest_Trueprop)) (Thm.concl_of distr_rule)
+      val concl = perhaps (try HOLogic.dest_Trueprop) (Thm.concl_of distr_rule)
     in
       (case concl of
         Const (\<^const_name>\<open>less_eq\<close>, _) $ (Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) $ _ =>
@@ -545,7 +553,7 @@
 fun add_no_code_type type_name context =
   Data.map (map_no_code_types (Symset.insert type_name)) context;
 
-fun is_no_code_type context type_name = (Symset.member o get_no_code_types) context type_name
+val is_no_code_type = Symset.member o get_no_code_types;
 
 
 (* setup fixed eq_onp rules *)
--- a/src/HOL/Tools/SMT/z3_replay_rules.ML	Tue May 16 23:41:20 2023 +0200
+++ b/src/HOL/Tools/SMT/z3_replay_rules.ML	Wed May 17 09:00:04 2023 +0200
@@ -26,7 +26,7 @@
 fun apply ctxt ct =
   let
     val net = Data.get (Context.Proof ctxt)
-    val xthms = Net.match_term net (Thm.term_of ct)
+    val xthms = map (Thm.transfer' ctxt) (Net.match_term net (Thm.term_of ct))
 
     fun select ct = map_filter (maybe_instantiate ct) xthms
     fun select' ct =
@@ -40,14 +40,12 @@
 fun ins thm net = Net.insert_term Thm.eq_thm (prep thm) net handle Net.INSERT => net
 fun del thm net = Net.delete_term Thm.eq_thm (prep thm) net handle Net.DELETE => net
 
-val add = Thm.declaration_attribute (Data.map o ins)
+val add = Thm.declaration_attribute (Data.map o ins o Thm.trim_context)
 val del = Thm.declaration_attribute (Data.map o del)
 
-val name = Binding.name "z3_rule"
-
-val description = "declaration of Z3 proof rules"
-
-val _ = Theory.setup (Attrib.setup name (Attrib.add_del add del) description #>
-  Global_Theory.add_thms_dynamic (name, Net.content o Data.get))
+val _ = Theory.setup
+ (Attrib.setup \<^binding>\<open>z3_rule\<close> (Attrib.add_del add del) "declaration of Z3 proof rules" #>
+  Global_Theory.add_thms_dynamic (\<^binding>\<open>z3_rule\<close>,
+    fn context => map (Thm.transfer'' context) (Net.content (Data.get context))))
 
 end;
--- a/src/Pure/Concurrent/thread_position.ML	Tue May 16 23:41:20 2023 +0200
+++ b/src/Pure/Concurrent/thread_position.ML	Wed May 17 09:00:04 2023 +0200
@@ -6,7 +6,7 @@
 
 signature THREAD_POSITION =
 sig
-  type T = {line: int, offset: int, end_offset: int, props: {file: string, id: string}}
+  type T = {line: int, offset: int, end_offset: int, props: {label: string, file: string, id: string}}
   val none: T
   val get: unit -> T
   val setmp: T -> ('a -> 'b) -> 'a -> 'b
@@ -15,11 +15,11 @@
 structure Thread_Position: THREAD_POSITION =
 struct
 
-type T = {line: int, offset: int, end_offset: int, props: {file: string, id: string}};
+type T = {line: int, offset: int, end_offset: int, props: {label: string, file: string, id: string}};
 
 val var = Thread_Data.var () : T Thread_Data.var;
 
-val none: T = {line = 0, offset = 0, end_offset = 0, props = {file = "", id = ""}};
+val none: T = {line = 0, offset = 0, end_offset = 0, props = {label = "", file = "", id = ""}};
 
 fun get () = (case Thread_Data.get var of NONE => none | SOME pos => pos);
 fun setmp pos f x = Thread_Data.setmp var (if pos = none then NONE else SOME pos) f x;
--- a/src/Pure/Concurrent/unsynchronized.ML	Tue May 16 23:41:20 2023 +0200
+++ b/src/Pure/Concurrent/unsynchronized.ML	Wed May 17 09:00:04 2023 +0200
@@ -18,6 +18,7 @@
   type 'a weak_ref = 'a ref option ref
   val weak_ref: 'a -> 'a weak_ref
   val weak_peek: 'a weak_ref -> 'a option
+  val weak_active: 'a weak_ref -> bool
 end;
 
 structure Unsynchronized: UNSYNCHRONIZED =
@@ -58,6 +59,9 @@
 fun weak_peek (ref (SOME (ref a))) = SOME a
   | weak_peek _ = NONE;
 
+fun weak_active (ref (SOME (ref _))) = true
+  | weak_active _ = false;
+
 end;
 
 ML_Name_Space.forget_val "ref";
--- a/src/Pure/General/position.ML	Tue May 16 23:41:20 2023 +0200
+++ b/src/Pure/General/position.ML	Wed May 17 09:00:04 2023 +0200
@@ -15,6 +15,7 @@
   val line_of: T -> int option
   val offset_of: T -> int option
   val end_offset_of: T -> int option
+  val label_of: T -> string option
   val file_of: T -> string option
   val id_of: T -> string option
   val symbol: Symbol.symbol -> T -> T
@@ -22,6 +23,7 @@
   val distance_of: T * T -> int option
   val none: T
   val start: T
+  val label: string -> T -> T
   val file_only: string -> T
   val file: string -> T
   val line_file_only: int -> string -> T
@@ -65,6 +67,7 @@
   val properties_of_range: range -> Properties.T
   val thread_data: unit -> T
   val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b
+  val setmp_thread_data_label: string -> ('a -> 'b) -> 'a -> 'b
   val default: T -> bool * T
 end;
 
@@ -83,6 +86,7 @@
    (int_ord o apply2 (#line o dest) |||
     int_ord o apply2 (#offset o dest) |||
     int_ord o apply2 (#end_offset o dest) |||
+    fast_string_ord o apply2 (#label o #props o dest) |||
     fast_string_ord o apply2 (#file o #props o dest) |||
     fast_string_ord o apply2 (#id o #props o dest));
 
@@ -99,6 +103,7 @@
 val offset_of = maybe_valid o #offset o dest;
 val end_offset_of = maybe_valid o #end_offset o dest;
 
+fun label_of (Pos {props = {label, ...}, ...}) = if label = "" then NONE else SOME label;
 fun file_of (Pos {props = {file, ...}, ...}) = if file = "" then NONE else SOME file;
 fun id_of (Pos {props = {id, ...}, ...}) = if id = "" then NONE else SOME id;
 
@@ -131,20 +136,23 @@
 
 (* make position *)
 
-type props = {file: string, id: string};
+type props = {label: string, file: string, id: string};
 
-val no_props: props = {file = "", id = ""};
+val no_props: props = {label = "", file = "", id = ""};
 
 fun file_props name : props =
-  if name = "" then no_props else {file = name, id = ""};
+  if name = "" then no_props else {label = "", file = name, id = ""};
 
 fun id_props id : props =
-  if id = "" then no_props else {file = "", id = id};
+  if id = "" then no_props else {label = "", file = "", id = id};
 
 
 val none = Pos {line = 0, offset = 0, end_offset = 0, props = no_props};
 val start = Pos {line = 1, offset = 1, end_offset = 0, props = no_props};
 
+fun label label (Pos {line, offset, end_offset, props = {label = _, file, id}}) =
+  Pos {line = line, offset = offset, end_offset = end_offset,
+    props = {label = label, file = file, id = id}};
 
 fun file_only name = Pos {line = 0, offset = 0, end_offset = 0, props = file_props name};
 fun file name = Pos {line = 1, offset = 1, end_offset = 0, props = file_props name};
@@ -156,9 +164,10 @@
 fun id id = Pos {line = 0, offset = 1, end_offset = 0, props = id_props id};
 fun id_only id = Pos {line = 0, offset = 0, end_offset = 0, props = id_props id};
 
-fun put_id id' (pos as Pos {line, offset, end_offset, props = {file, id}}) =
+fun put_id id' (pos as Pos {line, offset, end_offset, props = {label, file, id}}) =
   if id = id' then pos
-  else Pos {line = line, offset = offset, end_offset = end_offset, props = {file = file, id = id'}};
+  else Pos {line = line, offset = offset, end_offset = end_offset,
+    props = {label = label, file = file, id = id'}};
 
 fun copy_id pos = (case id_of pos of NONE => I | SOME id => put_id id);
 
@@ -196,7 +205,8 @@
 fun of_props {line, offset, end_offset, props} =
   Pos {line = line, offset = offset, end_offset = end_offset,
     props =
-     {file = Properties.get_string props Markup.fileN,
+     {label = Properties.get_string props Markup.labelN,
+      file = Properties.get_string props Markup.fileN,
       id = Properties.get_string props Markup.idN}};
 
 fun of_properties props =
@@ -206,10 +216,11 @@
     end_offset = Properties.get_int props Markup.end_offsetN,
     props = props};
 
-fun properties_of (Pos {line, offset, end_offset, props = {file, id}}) =
+fun properties_of (Pos {line, offset, end_offset, props = {label, file, id}}) =
   Properties.make_int Markup.lineN line @
   Properties.make_int Markup.offsetN offset @
   Properties.make_int Markup.end_offsetN end_offset @
+  Properties.make_string Markup.labelN label @
   Properties.make_string Markup.fileN file @
   Properties.make_string Markup.idN id;
 
@@ -309,6 +320,10 @@
 val thread_data = Pos o Thread_Position.get;
 fun setmp_thread_data pos = Thread_Position.setmp (dest pos);
 
+fun setmp_thread_data_label a f x =
+  if a = "" then f x
+  else setmp_thread_data (label a (thread_data ())) f x;
+
 fun default pos =
   if pos = none then (false, thread_data ())
   else (true, pos);
--- a/src/Pure/General/position.scala	Tue May 16 23:41:20 2023 +0200
+++ b/src/Pure/General/position.scala	Wed May 17 09:00:04 2023 +0200
@@ -15,6 +15,7 @@
   val Line = new Properties.Int(Markup.LINE)
   val Offset = new Properties.Int(Markup.OFFSET)
   val End_Offset = new Properties.Int(Markup.END_OFFSET)
+  val Label = new Properties.String(Markup.LABEL)
   val File = new Properties.String(Markup.FILE)
   val Id = new Properties.Long(Markup.ID)
   val Id_String = new Properties.String(Markup.ID)
@@ -22,6 +23,7 @@
   val Def_Line = new Properties.Int(Markup.DEF_LINE)
   val Def_Offset = new Properties.Int(Markup.DEF_OFFSET)
   val Def_End_Offset = new Properties.Int(Markup.DEF_END_OFFSET)
+  val Def_Label = new Properties.String(Markup.DEF_LABEL)
   val Def_File = new Properties.String(Markup.DEF_FILE)
   val Def_Id = new Properties.Long(Markup.DEF_ID)
 
--- a/src/Pure/Isar/attrib.ML	Tue May 16 23:41:20 2023 +0200
+++ b/src/Pure/Isar/attrib.ML	Wed May 17 09:00:04 2023 +0200
@@ -163,8 +163,14 @@
 (* get attributes *)
 
 fun attribute_generic context =
-  let val table = Attributes.get context
-  in fn src => #1 (Name_Space.get table (#1 (Token.name_of_src src))) src end;
+  let val table = Attributes.get context in
+    fn src =>
+      let
+        val name = #1 (Token.name_of_src src);
+        val label = Long_Name.qualify Markup.attributeN name;
+        val att = #1 (Name_Space.get table name) src;
+      in Position.setmp_thread_data_label label att end
+  end;
 
 val attribute = attribute_generic o Context.Proof;
 val attribute_global = attribute_generic o Context.Theory;
--- a/src/Pure/Isar/local_theory.ML	Tue May 16 23:41:20 2023 +0200
+++ b/src/Pure/Isar/local_theory.ML	Wed May 17 09:00:04 2023 +0200
@@ -43,6 +43,7 @@
   val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
   val target_morphism: local_theory -> morphism
   val propagate_ml_env: generic_theory -> generic_theory
+  val touch_ml_env: generic_theory -> generic_theory
   val operations_of: local_theory -> operations
   val define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory
@@ -253,6 +254,13 @@
       end
   | propagate_ml_env context = context;
 
+fun touch_ml_env context =
+  if Context.enabled_tracing () then
+    (case context of
+      Context.Theory _ => ML_Env.touch context
+    | Context.Proof _ => context)
+  else context;
+
 
 
 (** operations **)
--- a/src/Pure/Isar/outer_syntax.ML	Tue May 16 23:41:20 2023 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Wed May 17 09:00:04 2023 +0200
@@ -325,7 +325,8 @@
   command ("ML", \<^here>) "ML text within theory or local theory"
     (Parse.ML_source >> (fn source =>
       Toplevel.generic_theory
-        (ML_Context.exec (fn () =>
+        (Local_Theory.touch_ml_env #>
+          ML_Context.exec (fn () =>
             ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source) #>
           Local_Theory.propagate_ml_env)));
 
--- a/src/Pure/Isar/proof_display.ML	Tue May 16 23:41:20 2023 +0200
+++ b/src/Pure/Isar/proof_display.ML	Wed May 17 09:00:04 2023 +0200
@@ -28,6 +28,9 @@
     ((string * string) * (string * thm list) list) -> unit
   val print_consts: bool -> Position.T -> Proof.context ->
     (string * typ -> bool) -> (string * typ) list -> unit
+  val markup_extern_label: Position.T -> (Markup.T * xstring) option
+  val print_label: Position.T -> string
+  val print_context_tracing: Context.generic * Position.T -> string
 end
 
 structure Proof_Display: PROOF_DISPLAY =
@@ -390,4 +393,30 @@
 
 end;
 
+
+(* position label *)
+
+val command_prefix = Markup.commandN ^ ".";
+
+fun markup_extern_label pos =
+  Position.label_of pos |> Option.map (fn label =>
+    (case try (unprefix command_prefix) label of
+      SOME cmd => (Markup.keyword1, Long_Name.base_name cmd)
+    | NONE => (Markup.empty, label)));
+
+fun print_label pos =
+  (case markup_extern_label pos of
+    NONE => ""
+  | SOME (m, s) => Markup.markup m s);
+
+
+(* context tracing *)
+
+fun context_type (Context.Theory _) = "theory"
+  | context_type (Context.Proof ctxt) =
+      if can Local_Theory.assert ctxt then "local_theory" else "Proof.context";
+
+fun print_context_tracing (context, pos) =
+  context_type context ^ (case print_label pos of "" => "" | s => " " ^ s) ^ Position.here pos;
+
 end;
--- a/src/Pure/Isar/toplevel.ML	Tue May 16 23:41:20 2023 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed May 17 09:00:04 2023 +0200
@@ -610,8 +610,8 @@
   let val put_id = Position.put_id (Document_ID.print id)
   in position (put_id pos) tr end;
 
-fun setmp_thread_position (Transition {pos, ...}) f x =
-  Position.setmp_thread_data pos f x;
+fun setmp_thread_position (Transition {pos, name, ...}) f x =
+  Position.setmp_thread_data (Position.label (Long_Name.qualify Markup.commandN name) pos) f x;
 
 
 (* apply transitions *)
--- a/src/Pure/ML/ml_compiler.ML	Tue May 16 23:41:20 2023 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Wed May 17 09:00:04 2023 +0200
@@ -166,7 +166,8 @@
     (* input *)
 
     val position_props =
-      filter (fn (a, _) => a = Markup.idN orelse a = Markup.fileN) (Position.properties_of pos);
+      filter (fn (a, _) => a = Markup.labelN orelse a = Markup.fileN orelse a = Markup.idN)
+        (Position.properties_of pos);
     val location_props = op ^ (YXML.output_markup (":", position_props));
 
     val {explode_token, ...} = ML_Env.operations opt_context (#environment flags);
--- a/src/Pure/ML/ml_context.ML	Tue May 16 23:41:20 2023 +0200
+++ b/src/Pure/ML/ml_context.ML	Wed May 17 09:00:04 2023 +0200
@@ -228,7 +228,9 @@
     SOME context' => context'
   | NONE => error "Missing context after execution");
 
-fun expression pos ants = exec (fn () => eval ML_Compiler.flags pos ants);
+fun expression pos ants =
+  Local_Theory.touch_ml_env #>
+  exec (fn () => eval ML_Compiler.flags pos ants);
 
 end;
 
--- a/src/Pure/ML/ml_env.ML	Tue May 16 23:41:20 2023 +0200
+++ b/src/Pure/ML/ml_env.ML	Wed May 17 09:00:04 2023 +0200
@@ -26,6 +26,7 @@
   val Isabelle_operations: operations
   val SML_operations: operations
   val operations: Context.generic option -> string -> operations
+  val touch: Context.generic -> Context.generic
   val forget_structure: string -> Context.generic -> Context.generic
   val bootstrap_name_space: Context.generic -> Context.generic
   val add_name_space: string -> ML_Name_Space.T -> Context.generic -> Context.generic
@@ -127,6 +128,8 @@
 val get_env = Name_Space.get o #1 o Data.get;
 val get_tables = #1 oo get_env;
 
+val touch = Data.map I;
+
 fun update_tables env_name f context = context |> (Data.map o apfst) (fn envs =>
   let val _ = Name_Space.get envs env_name;
   in Name_Space.map_table_entry env_name (apfst f) envs end);
--- a/src/Pure/ML/ml_file.ML	Tue May 16 23:41:20 2023 +0200
+++ b/src/Pure/ML/ml_file.ML	Wed May 17 09:00:04 2023 +0200
@@ -28,6 +28,7 @@
         debug = debug, writeln = writeln, warning = warning};
   in
     gthy
+    |> Local_Theory.touch_ml_env
     |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
     |> Local_Theory.propagate_ml_env
     |> Context.mapping provide (Local_Theory.background_theory provide)
--- a/src/Pure/PIDE/markup.ML	Tue May 16 23:41:20 2023 +0200
+++ b/src/Pure/PIDE/markup.ML	Wed May 17 09:00:04 2023 +0200
@@ -58,6 +58,7 @@
   val end_lineN: string
   val offsetN: string
   val end_offsetN: string
+  val labelN: string
   val fileN: string
   val idN: string
   val positionN: string val position: T
@@ -408,12 +409,13 @@
 val offsetN = "offset";
 val end_offsetN = "end_offset";
 
+val labelN = "label";
 val fileN = "file";
 val idN = "id";
 
 val (positionN, position) = markup_elem "position";
 
-val position_properties = [lineN, offsetN, end_offsetN, fileN, idN];
+val position_properties = [lineN, offsetN, end_offsetN, labelN, fileN, idN];
 fun position_property (entry: Properties.entry) = member (op =) position_properties (#1 entry);
 
 
--- a/src/Pure/PIDE/markup.scala	Tue May 16 23:41:20 2023 +0200
+++ b/src/Pure/PIDE/markup.scala	Wed May 17 09:00:04 2023 +0200
@@ -137,18 +137,20 @@
   val END_LINE = "line"
   val OFFSET = "offset"
   val END_OFFSET = "end_offset"
+  val LABEL = "label"
   val FILE = "file"
   val ID = "id"
 
   val DEF_LINE = "def_line"
   val DEF_OFFSET = "def_offset"
   val DEF_END_OFFSET = "def_end_offset"
+  val DEF_LABEL = "def_label"
   val DEF_FILE = "def_file"
   val DEF_ID = "def_id"
 
   val POSITION = "position"
 
-  val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
+  val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, LABEL, FILE, ID)
   def position_property(entry: Properties.Entry): Boolean = POSITION_PROPERTIES(entry._1)
 
 
@@ -156,7 +158,7 @@
 
   private val def_names: Map[String, String] =
     Map(LINE -> DEF_LINE, OFFSET -> DEF_OFFSET, END_OFFSET -> DEF_END_OFFSET,
-      FILE -> DEF_FILE, ID -> DEF_ID)
+      LABEL -> DEF_LABEL, FILE -> DEF_FILE, ID -> DEF_ID)
 
   def def_name(a: String): String = def_names.getOrElse(a, a + "def_")
 
--- a/src/Pure/PIDE/session.ML	Tue May 16 23:41:20 2023 +0200
+++ b/src/Pure/PIDE/session.ML	Wed May 17 09:00:04 2023 +0200
@@ -11,6 +11,7 @@
   val welcome: unit -> string
   val shutdown: unit -> unit
   val finish: unit -> unit
+  val print_context_tracing: (Context.generic -> bool) -> unit
 end;
 
 structure Session: SESSION =
@@ -40,6 +41,11 @@
  (shutdown ();
   Par_List.map (Global_Theory.get_thm_names o Thy_Info.get_theory) (Thy_Info.get_names ());
   Thy_Info.finish ();
-  shutdown ());
+  shutdown ();
+  ignore (Context.finish_tracing ()));
+
+fun print_context_tracing pred =
+  List.app (writeln o Proof_Display.print_context_tracing)
+    (filter (pred o #1) (#contexts (Context.finish_tracing ())));
 
 end;
--- a/src/Pure/System/isabelle_process.ML	Tue May 16 23:41:20 2023 +0200
+++ b/src/Pure/System/isabelle_process.ML	Wed May 17 09:00:04 2023 +0200
@@ -200,7 +200,10 @@
   if Options.default_bool "export_standard_proofs" then Proofterm.proofs := 2 else ();
   let val proofs = Options.default_int "record_proofs"
   in if proofs < 0 then () else Proofterm.proofs := proofs end;
-  Printer.show_markup_default := false);
+  Printer.show_markup_default := false;
+  Context.theory_tracing := Options.default_bool "context_theory_tracing";
+  Context.proof_tracing := Options.default_bool "context_proof_tracing";
+  Context.data_timing := Options.default_bool "context_data_timing");
 
 fun init_options_interactive () =
  (init_options ();
--- a/src/Pure/Thy/thy_info.ML	Tue May 16 23:41:20 2023 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed May 17 09:00:04 2023 +0200
@@ -44,7 +44,7 @@
     val props' = Position.properties_of (#adjust_pos context pos);
   in
     filter (fn (a, _) => a = Markup.offsetN orelse a = Markup.end_offsetN) props' @
-    filter (fn (a, _) => a = Markup.idN orelse a = Markup.fileN) props
+    filter (fn (a, _) => a = Markup.labelN orelse a = Markup.fileN orelse a = Markup.idN) props
   end;
 
 structure Presentation = Theory_Data
--- a/src/Pure/context.ML	Tue May 16 23:41:20 2023 +0200
+++ b/src/Pure/context.ML	Wed May 17 09:00:04 2023 +0200
@@ -34,7 +34,7 @@
   type id = int
   type theory_id
   val theory_id: theory -> theory_id
-  val timing: bool Unsynchronized.ref
+  val data_timing: bool Unsynchronized.ref
   val parents_of: theory -> theory list
   val ancestors_of: theory -> theory list
   val theory_id_ord: theory_id ord
@@ -67,9 +67,10 @@
   val join_certificate: certificate * certificate -> certificate
   (*generic context*)
   datatype generic = Theory of theory | Proof of Proof.context
-  val trace_theories: bool Unsynchronized.ref
-  val trace_proofs: bool Unsynchronized.ref
-  val allocations_trace: unit ->
+  val theory_tracing: bool Unsynchronized.ref
+  val proof_tracing: bool Unsynchronized.ref
+  val enabled_tracing: unit -> bool
+  val finish_tracing: unit ->
    {contexts: (generic * Position.T) list,
     active_contexts: int,
     active_theories: int,
@@ -195,55 +196,57 @@
 
 (* heap allocations *)
 
-val trace_theories = Unsynchronized.ref false;
-val trace_proofs = Unsynchronized.ref false;
+val theory_tracing = Unsynchronized.ref false;
+val proof_tracing = Unsynchronized.ref false;
+
+fun enabled_tracing () = ! theory_tracing orelse ! proof_tracing;
 
 local
 
+fun cons_tokens var token =
+  Synchronized.change var (fn (n, tokens) => (n + 1, Weak.weak (SOME token) :: tokens));
+
+fun finish_tokens var =
+  Synchronized.change_result var (fn (n, tokens) =>
+    let
+      val tokens' = filter Unsynchronized.weak_active tokens;
+      val results = map_filter Unsynchronized.weak_peek tokens';
+    in ((n, results), (n, tokens')) end);
+
 fun make_token guard var token0 =
   if ! guard then
     let
       val token = Unsynchronized.ref (! token0);
       val pos = Position.thread_data ();
-      fun assign res =
-        (token := res; Synchronized.change var (cons (Weak.weak (SOME token))); res);
+      fun assign res = (token := res; cons_tokens var token; res);
     in (token, pos, assign) end
   else (token0, Position.none, I);
 
-val theory_tokens = Synchronized.var "theory_tokens" ([]: theory Unsynchronized.weak_ref list);
-val proof_tokens = Synchronized.var "proof_tokens" ([]: Proof.context Unsynchronized.weak_ref list);
+val theory_tokens = Synchronized.var "theory_tokens" (0, []: theory Unsynchronized.weak_ref list);
+val proof_tokens = Synchronized.var "proof_tokens" (0, []: proof Unsynchronized.weak_ref list);
 
 val theory_token0 = Unsynchronized.ref Thy_Undef;
 val proof_token0 = Unsynchronized.ref Prf_Undef;
 
 in
 
-fun theory_token () = make_token trace_theories theory_tokens theory_token0;
-fun proof_token () = make_token trace_proofs proof_tokens proof_token0;
+fun theory_token () = make_token theory_tracing theory_tokens theory_token0;
+fun proof_token () = make_token proof_tracing proof_tokens proof_token0;
 
-fun allocations_trace () =
+fun finish_tracing () =
   let
     val _ = ML_Heap.full_gc ();
-    val trace1 = Synchronized.value theory_tokens;
-    val trace2 = Synchronized.value proof_tokens;
+    val (total_theories, token_theories) = finish_tokens theory_tokens;
+    val (total_proofs, token_proofs) = finish_tokens proof_tokens;
 
-    fun cons1 r =
-      (case Unsynchronized.weak_peek r of
-        SOME (thy as Thy (_, {theory_token_pos, ...}, _, _)) =>
-          cons (Theory thy, theory_token_pos)
-      | _ => I);
-    fun cons2 r =
-      (case Unsynchronized.weak_peek r of
-        SOME (ctxt as Prf (_, proof_token_pos, _, _)) =>
-          cons (Proof ctxt, proof_token_pos)
-      | _ => I);
+    fun cons1 (thy as Thy (_, {theory_token_pos, ...}, _, _)) = cons (Theory thy, theory_token_pos)
+      | cons1 _ = I;
+    fun cons2 (ctxt as Prf (_, proof_token_pos, _, _)) = cons (Proof ctxt, proof_token_pos)
+      | cons2 _ = I;
 
-    val contexts = build (fold cons1 trace1 #> fold cons2 trace2);
+    val contexts = build (fold cons1 token_theories #> fold cons2 token_proofs);
     val active_theories = fold (fn (Theory _, _) => Integer.add 1 | _ => I) contexts 0;
     val active_proofs = fold (fn (Proof _, _) => Integer.add 1 | _ => I) contexts 0;
-
-    val total_theories = length trace1;
-    val total_proofs = length trace2;
   in
     {contexts = contexts,
      active_contexts = active_theories + active_proofs,
@@ -368,7 +371,7 @@
 
 (* data kinds and access methods *)
 
-val timing = Unsynchronized.ref false;
+val data_timing = Unsynchronized.ref false;
 
 local
 
@@ -393,7 +396,7 @@
 val invoke_empty = #empty o the_kind;
 
 fun invoke_merge kind args =
-  if ! timing then
+  if ! data_timing then
     Timing.cond_timeit true ("Theory_Data.merge" ^ Position.here (#pos kind))
       (fn () => #merge kind args)
   else #merge kind args;
--- a/src/Pure/thm.ML	Tue May 16 23:41:20 2023 +0200
+++ b/src/Pure/thm.ML	Wed May 17 09:00:04 2023 +0200
@@ -992,7 +992,8 @@
       let
         val {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop} = args;
 
-        val thy = Context.certificate_theory cert;
+        val thy = Context.certificate_theory cert
+          handle ERROR msg => raise CONTEXT (msg, [], [], [thm], NONE);
         val bad_thys =
           constraints |> map_filter (fn {theory = thy', ...} =>
             if Context.eq_thy (thy, thy') then NONE else SOME thy');
@@ -1558,8 +1559,9 @@
                 (*remove trivial tpairs, of the form t \<equiv> t*)
                 |> filter_out (op aconv);
               val der' = deriv_rule1 (Proofterm.norm_proof' env) der;
-              val constraints' =
-                insert_constraints_env (Context.certificate_theory cert') env constraints;
+              val thy' = Context.certificate_theory cert' handle ERROR msg =>
+                raise CONTEXT (msg, [], [], [th], Option.map Context.Proof opt_ctxt);
+              val constraints' = insert_constraints_env thy' env constraints;
               val prop' = Envir.norm_term env prop;
               val maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop');
               val shyps = Envir.insert_sorts env shyps;
@@ -1699,7 +1701,8 @@
       val (tpairs', maxidx') =
         fold_map (fn (t, u) => fn i => subst t i ||>> subst u) tpairs maxidx1;
 
-      val thy' = Context.certificate_theory cert';
+      val thy' = Context.certificate_theory cert'
+        handle ERROR msg => raise CONTEXT (msg, [], [], [th], NONE);
       val constraints' =
         TVars.fold (fn ((_, S), (T, _)) => insert_constraints thy' (T, S))
           instT' constraints;
@@ -1927,12 +1930,14 @@
         val normt = Envir.norm_term env;
         fun assumption_proof prf =
           Proofterm.assumption_proof (map normt Bs) (normt Bi) n prf;
+        val thy' = Context.certificate_theory cert' handle ERROR msg =>
+          raise CONTEXT (msg, [], [], [state], Option.map Context.Proof opt_ctxt);
       in
         Thm (deriv_rule1
           (assumption_proof #> not (Envir.is_empty env) ? Proofterm.norm_proof' env) der,
          {tags = [],
           maxidx = Envir.maxidx_of env,
-          constraints = insert_constraints_env (Context.certificate_theory cert') env constraints,
+          constraints = insert_constraints_env thy' env constraints,
           shyps = Envir.insert_sorts env shyps,
           hyps = hyps,
           tpairs = if Envir.is_empty env then tpairs else map (apply2 normt) tpairs,
@@ -2174,9 +2179,11 @@
                 else (*normalize the new rule fully*)
                   (ntps, (map normt (Bs @ As), normt C))
              end
+           val thy' = Context.certificate_theory cert handle ERROR msg =>
+            raise CONTEXT (msg, [], [], [state, orule], Option.map Context.Proof opt_ctxt);
            val constraints' =
              union_constraints constraints1 constraints2
-             |> insert_constraints_env (Context.certificate_theory cert) env;
+             |> insert_constraints_env thy' env;
            fun bicompose_proof prf1 prf2 =
              Proofterm.bicompose_proof flatten (map normt Bs) (map normt As) A oldAs n (nlift+1)
                prf1 prf2
--- a/src/Tools/Haskell/Haskell.thy	Tue May 16 23:41:20 2023 +0200
+++ b/src/Tools/Haskell/Haskell.thy	Wed May 17 09:00:04 2023 +0200
@@ -732,7 +732,7 @@
 
   completionN, completion, no_completionN, no_completion,
 
-  lineN, end_lineN, offsetN, end_offsetN, fileN, idN, positionN, position,
+  lineN, end_lineN, offsetN, end_offsetN, labelN, fileN, idN, positionN, position,
   position_properties, def_name,
 
   expressionN, expression,
@@ -866,7 +866,8 @@
 offsetN = \<open>Markup.offsetN\<close>
 end_offsetN = \<open>Markup.end_offsetN\<close>
 
-fileN, idN :: Bytes
+labelN, fileN, idN :: Bytes
+labelN = \<open>Markup.labelN\<close>
 fileN = \<open>Markup.fileN\<close>
 idN = \<open>Markup.idN\<close>
 
@@ -876,7 +877,7 @@
 position = markup_elem positionN
 
 position_properties :: [Bytes]
-position_properties = [lineN, offsetN, end_offsetN, fileN, idN]
+position_properties = [lineN, offsetN, end_offsetN, labelN, fileN, idN]
 
 
 {- position "def" names -}
@@ -1283,6 +1284,7 @@
     _column :: Int,
     _offset :: Int,
     _end_offset :: Int,
+    _label :: Bytes,
     _file :: Bytes,
     _id :: Bytes }
   deriving (Eq, Ord)
@@ -1306,6 +1308,9 @@
 offset_of = maybe_valid . _offset
 end_offset_of = maybe_valid . _end_offset
 
+label_of :: T -> Maybe Bytes
+label_of = proper_string . _label
+
 file_of :: T -> Maybe Bytes
 file_of = proper_string . _file
 
@@ -1316,10 +1321,13 @@
 {- make position -}
 
 start :: T
-start = Position 1 1 1 0 Bytes.empty Bytes.empty
+start = Position 1 1 1 0 Bytes.empty Bytes.empty Bytes.empty
 
 none :: T
-none = Position 0 0 0 0 Bytes.empty Bytes.empty
+none = Position 0 0 0 0 Bytes.empty Bytes.empty Bytes.empty
+
+label :: Bytes -> T -> T
+label label pos = pos { _label = label }
 
 put_file :: Bytes -> T -> T
 put_file file pos = pos { _file = file }
@@ -1392,6 +1400,7 @@
     _line = get_int props Markup.lineN,
     _offset = get_int props Markup.offsetN,
     _end_offset = get_int props Markup.end_offsetN,
+    _label = get_string props Markup.labelN,
     _file = get_string props Markup.fileN,
     _id = get_string props Markup.idN }
 
@@ -1406,6 +1415,7 @@
   int_entry Markup.lineN (_line pos) ++
   int_entry Markup.offsetN (_offset pos) ++
   int_entry Markup.end_offsetN (_end_offset pos) ++
+  string_entry Markup.labelN (_label pos) ++
   string_entry Markup.fileN (_file pos) ++
   string_entry Markup.idN (_id pos)
 
--- a/src/ZF/Tools/induct_tacs.ML	Tue May 16 23:41:20 2023 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Wed May 17 09:00:04 2023 +0200
@@ -157,8 +157,8 @@
     thy
     |> Sign.add_path (Long_Name.base_name big_rec_name)
     |> Global_Theory.add_thmss [((Binding.name "simps", simps), [Simplifier.simp_add])] |> snd
-    |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
-    |> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
+    |> DatatypesData.map (Symtab.update (big_rec_name, dt_info))
+    |> ConstructorsData.map (fold_rev Symtab.update con_pairs)
     |> Sign.parent_path
   end;
 
--- a/src/ZF/Tools/inductive_package.ML	Tue May 16 23:41:20 2023 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Wed May 17 09:00:04 2023 +0200
@@ -274,6 +274,7 @@
     |> Global_Theory.add_thm
       ((Binding.name "elim",
         rule_by_tactic ctxt3 (basic_elim_tac ctxt3) (unfold RS Ind_Syntax.equals_CollectD)), []);
+  val elim' = Thm.trim_context elim;
 
   val ctxt4 = Proof_Context.init_global thy4;
 
@@ -284,7 +285,7 @@
   fun make_cases ctxt A =
     rule_by_tactic ctxt
       (basic_elim_tac ctxt THEN ALLGOALS (asm_full_simp_tac ctxt) THEN basic_elim_tac ctxt)
-      (Thm.assume A RS elim)
+      (Thm.assume A RS Thm.transfer' ctxt elim')
       |> Drule.export_without_context_open;
 
   fun induction_rules raw_induct =