# HG changeset patch # User desharna # Date 1684306804 -7200 # Node ID ab8310c0e6d9d5c6a9994df9dac856fd48a2d4dc # Parent 8122e865687eba9cd54088c931ed277583ced675# Parent 37894dff0111101415bedcc88781707580944b06 merged diff -r 8122e865687e -r ab8310c0e6d9 etc/options --- 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" diff -r 8122e865687e -r ab8310c0e6d9 src/FOL/ex/Locale_Test/Locale_Test1.thy --- 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) \h(prod(x, y)) = sum(h(x), h(y))\ by (rule semi_hom_mult) diff -r 8122e865687e -r ab8310c0e6d9 src/HOL/Analysis/Abstract_Topological_Spaces.thy --- 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) \ - topspace(prod_topology X Y) = {} \ connected_space X \ 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 \ {}" "topspace Y \ {}" - 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 \ topspace Y \ U \ V" "U \ V = {}" - and "U \ {}" and "V \ {}" - for U V - proof - - have Usub: "U \ topspace X \ topspace Y" and Vsub: "V \ topspace X \ topspace Y" - using that by (metis openin_subset topspace_prod_topology)+ - obtain a b where ab: "(a,b) \ U" and a: "a \ topspace X" and b: "b \ topspace Y" - using \U \ {}\ Usub by auto - have "\ topspace X \ topspace Y \ U" - using Usub Vsub \U \ V = {}\ \V \ {}\ by auto - then obtain x y where x: "x \ topspace X" and y: "y \ topspace Y" and "(x,y) \ U" - by blast - have oX: "openin X {x \ topspace X. (x,y) \ U}" "openin X {x \ topspace X. (x,y) \ V}" - and oY: "openin Y {y \ topspace Y. (a,y) \ U}" "openin Y {y \ topspace Y. (a,y) \ 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 \ {y \ topspace Y. (a,y) \ U} \ {y \ topspace Y. (a,y) \ V}" - using a that(3) by auto - have 2: "{y \ topspace Y. (a,y) \ U} \ {y \ topspace Y. (a,y) \ V} = {}" - using that(4) by auto - have 3: "{y \ topspace Y. (a,y) \ U} \ {}" - using ab b by auto - have 4: "{y \ topspace Y. (a,y) \ V} \ {}" - proof - - show ?thesis - using connected_spaceD [OF conX oX] UV \(x,y) \ U\ 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 \ T) \ - S = {} \ T = {} \ connectedin X S \ connectedin Y T" - by (force simp: connectedin_def subtopology_Times connected_space_prod_topology) - subsection\The notion of "separated between" (complement of "connected between)"\ diff -r 8122e865687e -r ab8310c0e6d9 src/HOL/Analysis/Abstract_Topology.thy --- 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: + "\closedin X S; S \ T\ \ 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: + "\quotient_map X X' q; connected_space X\ \ 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 \ connected_space X \ connected_space Y" unfolding homeomorphic_space_def homeomorphic_maps_def diff -r 8122e865687e -r ab8310c0e6d9 src/HOL/Analysis/Abstract_Topology_2.thy --- 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 @@ (\x. x / (1 + \x\)) (\y. y / (1 - \y\))" 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 + \x\) = y) \ (\y\ < 1 \ y / (1 - \y\) = x)" + using real_grow_shrink by (fastforce simp add: distrib_left) + +lemma real_shrink_lt: + fixes x::real + shows "x / (1 + \x\) < y / (1 + \y\) \ 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 + \x\) \ y / (1 + \y\) \ x \ y" + by (meson linorder_not_le real_shrink_lt) + +lemma real_shrink_grow: + fixes x::real + shows "\x\ < 1 \ x / (1 - \x\) / (1 + \x / (1 - \x\)\) = x" + using real_shrink_Galois by blast + +lemma continuous_shrink: + "continuous_on UNIV (\x::real. x / (1 + \x\))" + by (intro continuous_intros) auto + +lemma strict_mono_shrink: + "strict_mono (\x::real. x / (1 + \x\))" + by (simp add: monotoneI real_shrink_lt) + +lemma shrink_range: "(\x::real. x / (1 + \x\)) ` S \ {-1<..<1}" + by (auto simp: divide_simps) + +text \Note: connected sets of real numbers are the same thing as intervals\ +lemma connected_shrink: + fixes S :: "real set" + shows "connected ((\x. x / (1 + \x\)) ` S) \ connected S" (is "?lhs = ?rhs") +proof + assume "?lhs" + then have "connected ((\x. x / (1 - \x\)) ` (\x. x / (1 + \x\)) ` 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 diff -r 8122e865687e -r ab8310c0e6d9 src/HOL/Analysis/Elementary_Metric_Spaces.thy --- 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: "(\r>0. ball x r \ U) \ (\r>0. cball x r \ U)" + by (meson mem_interior mem_interior_cball) + subsection \Frontier\ diff -r 8122e865687e -r ab8310c0e6d9 src/HOL/Analysis/Locally.thy --- 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\Neighbourhood Bases\ @@ -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 \ S" and "a \ U" and "open U" + then obtain r where "r > 0" and r: "ball a r \ U" + by (metis open_contains_ball_eq) + show "\W. open W \ (\V. path_connectedin (top_of_set S) V \ a \ W \ S \ W \ V \ V \ S \ V \ U)" + proof (intro exI conjI) + show "path_connectedin (top_of_set S) (S \ ball a r)" + by (simp add: assms is_interval_Int is_interval_ball_real is_interval_path_connected path_connectedin_subtopology) + show "a \ ball a r" + by (simp add: \0 < r\) + qed (use \0 < r\ 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<.. + topspace (prod_topology X Y) = {} \ + locally_path_connected_space X \ 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 \ {}" "topspace Y \ {}" + 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) \ UV" + obtain A B where W12: "openin X A \ openin Y B \ x \ A \ y \ B \ A \ B \ UV" + using X Y by (metis UV \(x,y) \ UV\ openin_prod_topology_alt) + then obtain C D K L + where "openin X C" "path_connectedin X K" "x \ C" "C \ K" "K \ A" + "openin Y D" "path_connectedin Y L" "y \ D" "D \ L" "L \ B" + by (metis X Y locally_path_connected_space) + with W12 \openin X C\ \openin Y D\ + show "\U V. openin (prod_topology X Y) U \ path_connectedin (prod_topology X Y) V \ (x, y) \ U \ U \ V \ V \ UV" + apply (rule_tac x="C \ D" in exI) + apply (rule_tac x="K \ 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) \ + (\i \ 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: "\i\I. openin (X i) (W i)" + and "i \ I" and "x \ W i" + then obtain U V where U: "openin (X i) U" and V: "path_connectedin (X i) V" + and "x \ U" "U \ V" "V \ W i" + by (metis R \i \ I\ \x \ W i\ locally_path_connected_space) + show "\U. openin (sum_topology X I) U \ (\V. path_connectedin (sum_topology X I) V \ (i, x) \ U \ U \ V \ V \ Sigma I W)" + proof (intro exI conjI) + show "openin (sum_topology X I) (Pair i ` U)" + by (meson U \i \ I\ open_map_component_injection open_map_def) + show "path_connectedin (sum_topology X I) (Pair i ` V)" + by (meson V \i \ I\ continuous_map_component_injection path_connectedin_continuous_map_image) + show "Pair i ` V \ Sigma I W" + using \V \ W i\ \i \ I\ by force + qed (use \x \ U\ \U \ V\ in auto) + qed +qed + + +subsection\Locally connected spaces\ + +definition weakly_locally_connected_at + where "weakly_locally_connected_at x X \ neighbourhood_base_at x (connectedin X) X" + +definition locally_connected_at + where "locally_connected_at x X \ + neighbourhood_base_at x (\U. openin X U \ connectedin X U ) X" + +definition locally_connected_space + where "locally_connected_space X \ neighbourhood_base_of (connectedin X) X" + + +lemma locally_connected_A: "(\U x. openin X U \ x \ U + \ openin X (connected_component_of_set (subtopology X U) x)) + \ neighbourhood_base_of (\U. openin X U \ 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 \ + (\U x. openin X U \ x \ U \ 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 (\U. openin X U \ connectedin X U) X \ locally_connected_space X" + using locally_connected_space_def neighbourhood_base_of_mono by auto + + +lemma locally_connected_space_alt: + "locally_connected_space X \ neighbourhood_base_of (\U. openin X U \ 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 \ + (\U x. openin X U \ x \ U + \ 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 \ + (\V x. openin X V \ x \ V \ (\U. openin X U \ connectedin X U \ x \ U \ U \ 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 \ 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 \ + (\U C. openin X U \ C \ connected_components_of(subtopology X U) \ 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 \ 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: + "\locally_connected_space X; C \ connected_components_of X\ \ 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 \ + (\V. openin X V \ x \ V + \ (\U. openin X U \ x \ U \ U \ V \ + (\y \ U. \C. connectedin X C \ C \ V \ x \ C \ y \ 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 \ V" + then obtain U where "openin X U" "x \ U" "U \ V" + and U: "\y\U. \C. connectedin X C \ C \ V \ x \ C \ y \ C" + using R by force + show "\A B. openin X A \ connectedin X B \ x \ A \ A \ B \ B \ 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 \ 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 \ V" + using connected_component_of_subset_topspace by fastforce + qed (auto simp: \x \ U\ \openin X U\) + qed +qed + +lemma locally_connected_space_iff_weak: + "locally_connected_space X \ (\x \ 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 \ + (\V x. openin X V \ x \ V + \ (\U. openin X U \ x \ U \ U \ V \ + (\y \ U. \C. connectedin X C \ C \ V \ x \ C \ y \ C)))" + unfolding locally_connected_space_iff_weak weakly_locally_connected_at + using openin_subset subsetD by fastforce + +lemma locally_connected_space_open_subset: + "\locally_connected_space X; openin X S\ \ 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 \ connected_components_of (subtopology Y V)" + then have "C \ topspace Y" + using connected_components_of_subset by force + have ope1: "openin X {a \ topspace X. f a \ V}" + using \openin Y V\ f openin_continuous_map_preimage quotient_imp_continuous_map by blast + define Vf where "Vf \ {z \ topspace X. f z \ V}" + have "openin X {x \ topspace X. f x \ C}" + proof (clarsimp simp: openin_subopen [where S = "{x \ topspace X. f x \ C}"]) + fix x + assume "x \ topspace X" and "f x \ C" + show "\T. openin X T \ x \ T \ T \ {x \ topspace X. f x \ 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 \ connected_component_of_set (subtopology X Vf) x" + using C Vf_def \f x \ C\ \x \ topspace X\ connected_component_of_refl connected_components_of_subset by fastforce + have "connected_component_of_set (subtopology X Vf) x \ topspace X \ Vf" + using connected_component_of_subset_topspace by fastforce + moreover + have "f ` connected_component_of_set (subtopology X Vf) x \ C" + proof (rule connected_components_of_maximal [where X = "subtopology Y V"]) + show "C \ connected_components_of (subtopology Y V)" + by (simp add: C) + have \
: "quotient_map (subtopology X Vf) (subtopology Y V) f" + by (simp add: Vf_def \openin Y V\ 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 "\ disjnt C (f ` connected_component_of_set (subtopology X Vf) x)" + using \f x \ C\ x_in_conn by (auto simp: disjnt_iff) + qed + ultimately + show "connected_component_of_set (subtopology X Vf) x \ {x \ topspace X. f x \ C}" + by blast + qed + qed + then show "openin Y C" + using \C \ topspace Y\ f quotient_map_def by fastforce +qed + + +lemma locally_connected_space_retraction_map_image: + "\retraction_map X Y r; locally_connected_space X\ + \ 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 \ locally_connected_space X \ 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 \ 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<.. 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 + \ 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 \ connected_components_of (subtopology X S)" + shows "X interior_of C = C \ X interior_of S" +proof - + obtain Csub: "C \ topspace X" "C \ S" + by (meson C connectedin_connected_components_of connectedin_subset_topspace connectedin_subtopology) + show ?thesis + proof + show "X interior_of C \ C \ X interior_of S" + by (simp add: Csub interior_of_mono interior_of_subset) + have eq: "X interior_of S = \ (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 \ D \ X interior_of C" + if "D \ connected_components_of (subtopology X (X interior_of S))" for D + proof (cases "C \ D = {}") + case False + have "D \ 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 \ 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 \ X interior_of S \ 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 \ connected_components_of (subtopology X S)" + shows "X frontier_of C = C \ X frontier_of S" +proof - + obtain Csub: "C \ topspace X" "C \ S" + by (meson C connectedin_connected_components_of connectedin_subset_topspace connectedin_subtopology) + then have "X closure_of C - X interior_of C = C \ X closure_of S - C \ 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) \ + topspace (prod_topology X Y) = {} \ + locally_connected_space X \ 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 \ {}" "topspace Y \ {}" + 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) \ UV" + + obtain A B where W12: "openin X A \ openin Y B \ x \ A \ y \ B \ A \ B \ UV" + using X Y by (metis UV \(x,y) \ UV\ openin_prod_topology_alt) + then obtain C D K L + where "openin X C" "connectedin X K" "x \ C" "C \ K" "K \ A" + "openin Y D" "connectedin Y L" "y \ D" "D \ L" "L \ B" + by (metis X Y locally_connected_space) + with W12 \openin X C\ \openin Y D\ + show "\U V. openin (prod_topology X Y) U \ connectedin (prod_topology X Y) V \ (x, y) \ U \ U \ V \ V \ UV" + apply (rule_tac x="C \ D" in exI) + apply (rule_tac x="K \ 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) \ + topspace(product_topology X I) = {} \ + finite {i. i \ I \ ~connected_space(X i)} \ + (\i \ I. locally_connected_space(X i))" + (is "?lhs \ ?empty \ ?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 \ (\\<^sub>E i\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 \ U" "U \ C" and Csub: "C \ (\\<^sub>E i\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 \ I. V i \ topspace (X i)}" + and XV: "\i. i\I \ openin (X i) (V i)" and "z \ Pi\<^sub>E I V" and subU: "Pi\<^sub>E I V \ U" + by (force simp: openin_product_topology_alt) + show ?thesis + proof (intro conjI ballI) + have "connected_space (X i)" if "i \ I" "V i = topspace (X i)" for i + proof - + have pc: "connectedin (X i) ((\x. x i) ` C)" + apply (rule connectedin_continuous_map_image [OF _ V]) + by (simp add: continuous_map_product_projection \i \ I\) + moreover have "((\x. x i) ` C) = topspace (X i)" + proof + show "(\x. x i) ` C \ topspace (X i)" + by (simp add: pc connectedin_subset_topspace) + have "V i \ (\x. x i) ` (\\<^sub>E i\I. V i)" + by (metis \z \ Pi\<^sub>E I V\ empty_iff image_projection_PiE order_refl that(1)) + also have "\ \ (\x. x i) ` U" + using subU by blast + finally show "topspace (X i) \ (\x. x i) ` C" + using \U \ C\ that by blast + qed + ultimately show ?thesis + by (simp add: connectedin_topspace) + qed + then have "{i \ I. \ connected_space (X i)} \ {i \ I. V i \ topspace (X i)}" + by blast + with finV show "finite {i \ I. \ connected_space (X i)}" + using finite_subset by blast + next + show "locally_connected_space (X i)" if "i \ 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 \ F" + then obtain W where finW: "finite {i \ I. W i \ topspace (X i)}" + and opeW: "\i. i \ I \ openin (X i) (W i)" and "z \ Pi\<^sub>E I W" "Pi\<^sub>E I W \ F" + by (auto simp: openin_product_topology_alt) + have "\i \ I. \U C. openin (X i) U \ connectedin (X i) C \ z i \ U \ U \ C \ C \ W i \ + (W i = topspace (X i) \ + connected_space (X i) \ U = topspace (X i) \ C = topspace (X i))" + (is "\i \ I. ?\ i") + proof + fix i assume "i \ I" + have "locally_connected_space (X i)" + by (simp add: R \i \ I\) + moreover have "openin (X i) (W i) " "z i \ W i" + using \z \ Pi\<^sub>E I W\ opeW \i \ I\ by auto + ultimately obtain U C where UC: "openin (X i) U" "connectedin (X i) C" "z i \ U" "U \ C" "C \ W i" + using \i \ I\ by (force simp: locally_connected_space_def neighbourhood_base_of) + show "?\ i" + proof (cases "W i = topspace (X i) \ connected_space(X i)") + case True + then show ?thesis + using \z i \ W i\ connectedin_topspace by blast + next + case False + then show ?thesis + by (meson UC) + qed + qed + then obtain U C where + *: "\i. i \ I \ openin (X i) (U i) \ connectedin (X i) (C i) \ z i \ (U i) \ (U i) \ (C i) \ (C i) \ W i \ + (W i = topspace (X i) \ connected_space (X i) + \ (U i) = topspace (X i) \ (C i) = topspace (X i))" + by metis + let ?A = "{i \ I. \ connected_space (X i)} \ {i \ I. W i \ topspace (X i)}" + have "{i \ I. U i \ topspace (X i)} \ ?A" + by (clarsimp simp add: "*") + moreover have "finite ?A" + by (simp add: that finW) + ultimately have "finite {i \ I. U i \ 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 "\U. openin (product_topology X I) U \ + (\V. connectedin (product_topology X I) V \ z \ U \ U \ V \ V \ F)" + apply (rule_tac x="PiE I U" in exI, simp) + apply (rule_tac x="PiE I C" in exI) + using \z \ Pi\<^sub>E I W\ \Pi\<^sub>E I W \ F\ * + 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) \ + (\i \ 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: "\i\I. openin (X i) (W i)" + and "i \ I" and "x \ W i" + then obtain U V where U: "openin (X i) U" and V: "connectedin (X i) V" + and "x \ U" "U \ V" "V \ W i" + by (metis R \i \ I\ \x \ W i\ locally_connected_space) + show "\U. openin (sum_topology X I) U \ (\V. connectedin (sum_topology X I) V \ (i,x) \ U \ U \ V \ V \ Sigma I W)" + proof (intro exI conjI) + show "openin (sum_topology X I) (Pair i ` U)" + by (meson U \i \ I\ open_map_component_injection open_map_def) + show "connectedin (sum_topology X I) (Pair i ` V)" + by (meson V \i \ I\ continuous_map_component_injection connectedin_continuous_map_image) + show "Pair i ` V \ Sigma I W" + using \V \ W i\ \i \ I\ by force + qed (use \x \ U\ \U \ V\ in auto) + qed +qed + + end diff -r 8122e865687e -r ab8310c0e6d9 src/HOL/Analysis/Product_Topology.thy --- 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) \ + topspace(prod_topology X Y) = {} \ connected_space X \ 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 \ {}" "topspace Y \ {}" + 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 \ topspace Y \ U \ V" "U \ V = {}" + and "U \ {}" and "V \ {}" + for U V + proof - + have Usub: "U \ topspace X \ topspace Y" and Vsub: "V \ topspace X \ topspace Y" + using that by (metis openin_subset topspace_prod_topology)+ + obtain a b where ab: "(a,b) \ U" and a: "a \ topspace X" and b: "b \ topspace Y" + using \U \ {}\ Usub by auto + have "\ topspace X \ topspace Y \ U" + using Usub Vsub \U \ V = {}\ \V \ {}\ by auto + then obtain x y where x: "x \ topspace X" and y: "y \ topspace Y" and "(x,y) \ U" + by blast + have oX: "openin X {x \ topspace X. (x,y) \ U}" "openin X {x \ topspace X. (x,y) \ V}" + and oY: "openin Y {y \ topspace Y. (a,y) \ U}" "openin Y {y \ topspace Y. (a,y) \ 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 \ {y \ topspace Y. (a,y) \ U} \ {y \ topspace Y. (a,y) \ V}" + using a that(3) by auto + have 2: "{y \ topspace Y. (a,y) \ U} \ {y \ topspace Y. (a,y) \ V} = {}" + using that(4) by auto + have 3: "{y \ topspace Y. (a,y) \ U} \ {}" + using ab b by auto + have 4: "{y \ topspace Y. (a,y) \ V} \ {}" + proof - + show ?thesis + using connected_spaceD [OF conX oX] UV \(x,y) \ U\ 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 \ T) \ + S = {} \ T = {} \ connectedin X S \ connectedin Y T" + by (force simp: connectedin_def subtopology_Times connected_space_prod_topology) + end diff -r 8122e865687e -r ab8310c0e6d9 src/HOL/Analysis/Starlike.thy --- 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 \ closure S \ U \ 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" diff -r 8122e865687e -r ab8310c0e6d9 src/HOL/Analysis/Sum_Topology.thy --- 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: "\X S. \P X; closedin X S; openin X S\ \ P(subtopology X S)" + and PQ: "\X Y. X homeomorphic_space Y \ (P X \ Q Y)" + shows "(\i \ I. Q(X i))" +proof - + have "Q(X i)" if "i \ 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 diff -r 8122e865687e -r ab8310c0e6d9 src/HOL/Statespace/state_space.ML --- 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>\statespace_silent\ (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>\StateFun.lookup\ $ 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>\StateFun.lookup\ $ Syntax.const \<^const_syntax>\undefined\ $ 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>\StateFun.update\ $ Syntax.const \<^const_syntax>\undefined\ $ Syntax.const \<^const_syntax>\undefined\ $ Syntax.free n $ v $ s diff -r 8122e865687e -r ab8310c0e6d9 src/HOL/Tools/Lifting/lifting_info.ML --- 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>\less_eq\, _) $ (lhs as Const (\<^const_name>\relcompp\,_) $ _ $ _) $ 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>\less_eq\, _) $ (Const (\<^const_name>\relcompp\,_) $ _ $ _) $ _ => @@ -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 *) diff -r 8122e865687e -r ab8310c0e6d9 src/HOL/Tools/SMT/z3_replay_rules.ML --- 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>\z3_rule\ (Attrib.add_del add del) "declaration of Z3 proof rules" #> + Global_Theory.add_thms_dynamic (\<^binding>\z3_rule\, + fn context => map (Thm.transfer'' context) (Net.content (Data.get context)))) end; diff -r 8122e865687e -r ab8310c0e6d9 src/Pure/Concurrent/thread_position.ML --- 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; diff -r 8122e865687e -r ab8310c0e6d9 src/Pure/Concurrent/unsynchronized.ML --- 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"; diff -r 8122e865687e -r ab8310c0e6d9 src/Pure/General/position.ML --- 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); diff -r 8122e865687e -r ab8310c0e6d9 src/Pure/General/position.scala --- 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) diff -r 8122e865687e -r ab8310c0e6d9 src/Pure/Isar/attrib.ML --- 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; diff -r 8122e865687e -r ab8310c0e6d9 src/Pure/Isar/local_theory.ML --- 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 **) diff -r 8122e865687e -r ab8310c0e6d9 src/Pure/Isar/outer_syntax.ML --- 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))); diff -r 8122e865687e -r ab8310c0e6d9 src/Pure/Isar/proof_display.ML --- 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; diff -r 8122e865687e -r ab8310c0e6d9 src/Pure/Isar/toplevel.ML --- 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 *) diff -r 8122e865687e -r ab8310c0e6d9 src/Pure/ML/ml_compiler.ML --- 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); diff -r 8122e865687e -r ab8310c0e6d9 src/Pure/ML/ml_context.ML --- 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; diff -r 8122e865687e -r ab8310c0e6d9 src/Pure/ML/ml_env.ML --- 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); diff -r 8122e865687e -r ab8310c0e6d9 src/Pure/ML/ml_file.ML --- 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) diff -r 8122e865687e -r ab8310c0e6d9 src/Pure/PIDE/markup.ML --- 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); diff -r 8122e865687e -r ab8310c0e6d9 src/Pure/PIDE/markup.scala --- 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_") diff -r 8122e865687e -r ab8310c0e6d9 src/Pure/PIDE/session.ML --- 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; diff -r 8122e865687e -r ab8310c0e6d9 src/Pure/System/isabelle_process.ML --- 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 (); diff -r 8122e865687e -r ab8310c0e6d9 src/Pure/Thy/thy_info.ML --- 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 diff -r 8122e865687e -r ab8310c0e6d9 src/Pure/context.ML --- 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; diff -r 8122e865687e -r ab8310c0e6d9 src/Pure/thm.ML --- 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 \ 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 diff -r 8122e865687e -r ab8310c0e6d9 src/Tools/Haskell/Haskell.thy --- 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 = \Markup.offsetN\ end_offsetN = \Markup.end_offsetN\ -fileN, idN :: Bytes +labelN, fileN, idN :: Bytes +labelN = \Markup.labelN\ fileN = \Markup.fileN\ idN = \Markup.idN\ @@ -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) diff -r 8122e865687e -r ab8310c0e6d9 src/ZF/Tools/induct_tacs.ML --- 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; diff -r 8122e865687e -r ab8310c0e6d9 src/ZF/Tools/inductive_package.ML --- 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 =