# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1689182891 -3600
# Node ID 74c75da4cb01d0858a4f46dd2e3704d7661d955c
# Parent  021fb1b01de555461778f601c40abb4ca69bf48b
Some fixes, and SOME TIME LIMITS

diff -r 021fb1b01de5 -r 74c75da4cb01 src/HOL/Homology/Brouwer_Degree.thy
--- a/src/HOL/Homology/Brouwer_Degree.thy	Tue Jul 11 20:22:08 2023 +0100
+++ b/src/HOL/Homology/Brouwer_Degree.thy	Wed Jul 12 18:28:11 2023 +0100
@@ -1026,7 +1026,7 @@
     have rimeq: "r ` (topspace (subtopology (nsphere n) {x. x k \<le> 0}) \<inter> {x. x k = 0})
                = topspace (subtopology (nsphere n) {x. 0 \<le> x k}) \<inter> {x. x k = 0}"
       using continuous_map_eq_topcontinuous_at continuous_map_nsphere_reflection topcontinuous_at_atin
-      by (fastforce simp: r_def)
+      by (fastforce simp: r_def Pi_iff)
     show "?f \<in> iso ?G (relative_homology_group p (subtopology (nsphere n) {x. x k \<ge> 0}) {x. x k = 0})"
       using homeomorphic_map_relative_homology_iso [OF hmrs Int_lower1 rimeq]
       by (metis hom_induced_restrict relative_homology_group_restrict)
diff -r 021fb1b01de5 -r 74c75da4cb01 src/HOL/Homology/Homology_Groups.thy
--- a/src/HOL/Homology/Homology_Groups.thy	Tue Jul 11 20:22:08 2023 +0100
+++ b/src/HOL/Homology/Homology_Groups.thy	Wed Jul 12 18:28:11 2023 +0100
@@ -508,8 +508,8 @@
         hom_relmap p X (topspace X \<inter> S) Y (topspace Y \<inter> T) f c
            \<in> carrier (relative_homology_group p Y T)"
       for p X S Y f T c
-      using hom_carrier [OF 1 [of X Y f "topspace X \<inter> S" "topspace Y \<inter> T" p]]
-      by (simp add: image_subset_iff subtopology_restrict continuous_map_def)
+      using hom_carrier [OF 1 [of X Y f "topspace X \<inter> S" "topspace Y \<inter> T" p]] 
+            continuous_map_image_subset_topspace by fastforce
     have inhom: "(\<lambda>c. if continuous_map X Y f \<and> f ` (topspace X \<inter> S) \<subseteq> T \<and>
                       c \<in> carrier (relative_homology_group p X S)
             then hom_relmap p X (topspace X \<inter> S) Y (topspace Y \<inter> T) f c
@@ -530,10 +530,10 @@
         proof (cases "continuous_map X Y f")
           case True
           then have "f ` (topspace X \<inter> S) \<subseteq> topspace Y"
-            by (meson IntE continuous_map_def image_subsetI)
+            using continuous_map_image_subset_topspace by blast
           then show ?thesis
             using True False that
-          using 1 [of X Y f "topspace X \<inter> S" "topspace Y \<inter> T" p]
+            using 1 [of X Y f "topspace X \<inter> S" "topspace Y \<inter> T" p]
           by (simp add: 4 continuous_map_image_subset_topspace hom_mult not_less group.is_monoid monoid.m_closed Int_left_absorb)
         qed (simp add: group.is_monoid)
       qed
@@ -543,7 +543,7 @@
               f (homologous_rel_set p X S c) = homologous_rel_set p Y T (chain_map p f c)"
         for p X S Y T f c
       using 2 [of X Y f "topspace X \<inter> S" "topspace Y \<inter> T" p c]
-      by simp (meson IntE continuous_map_def image_subsetI)
+            continuous_map_image_subset_topspace by fastforce
     show ?thesis
       apply (rule_tac x="\<lambda>p X S Y T f c.
                if continuous_map X Y f \<and> f ` (topspace X \<inter> S) \<subseteq> T \<and>
diff -r 021fb1b01de5 -r 74c75da4cb01 src/HOL/Homology/Invariance_of_Domain.thy
--- a/src/HOL/Homology/Invariance_of_Domain.thy	Tue Jul 11 20:22:08 2023 +0100
+++ b/src/HOL/Homology/Invariance_of_Domain.thy	Wed Jul 12 18:28:11 2023 +0100
@@ -54,7 +54,7 @@
     moreover have "topspace (nsphere n) \<inter> {f. f n = 0} = topspace (nsphere (n - Suc 0))"
       by (metis subt_eq topspace_subtopology)
     ultimately show ?thesis
-      using cmr continuous_map_def by fastforce
+      using fim by auto
   qed
   then have fimeq: "f ` (topspace (nsphere n) \<inter> equator n) \<subseteq> topspace (nsphere n) \<inter> equator n"
     using fim cmf by (auto simp: equator_def continuous_map_def image_subset_iff)
@@ -623,7 +623,7 @@
         using rm_ret [OF \<open>squashable 0 UNIV\<close>] by auto
       then have "ret 0 x \<in> topspace (Euclidean_space n)"
         if "x \<in> topspace (Euclidean_space (Suc n))" "-1 < x n" "x n < 1" for x
-        using that by (simp add: continuous_map_def retraction_maps_def)
+        using that by (metis continuous_map_image_subset_topspace image_subset_iff retraction_maps_def)
       then show "(ret 0) ` (lo \<inter> hi) \<subseteq> topspace (Euclidean_space n) - S"
         by (auto simp: local.cong ret_def hi_def lo_def)
       show "homotopic_with (\<lambda>h. h ` (lo \<inter> hi) \<subseteq> lo \<inter> hi) (Euclidean_space (Suc n)) (Euclidean_space (Suc n)) (ret 0) id"
@@ -1353,7 +1353,7 @@
     have "openin (Euclidean_space n) (h ` e ` {- r<..<r})"
       unfolding 1
     proof (subst homeomorphic_map_openness [OF hom_e', symmetric])
-      show "h ` e ` {- r<..<r} \<subseteq> topspace (Euclidean_space 1)"
+      show hesub: "h ` e ` {- r<..<r} \<subseteq> topspace (Euclidean_space 1)"
         using "1" C_def \<open>\<And>r. B r \<subseteq> C r\<close> cmh continuous_map_image_subset_topspace eBr by fastforce
       have cont: "continuous_on {- r<..<r} (e' \<circ> h \<circ> e)"
       proof (intro continuous_on_compose)
@@ -1365,12 +1365,10 @@
           by (auto simp: eBr \<open>\<And>r. B r \<subseteq> C r\<close>) (auto simp: B_def)
         with cmh show "continuous_on (e ` {- r<..<r}) h"
           by (meson cm_Euclidean_space_iff_continuous_on continuous_on_subset)
-        have "h ` (e ` {- r<..<r}) \<subseteq> topspace ?E"
-          using subCr cmh by (simp add: continuous_map_def image_subset_iff)
-        moreover have "continuous_on (topspace ?E) e'"
+         have "continuous_on (topspace ?E) e'"
           by (metis "1" continuous_map_Euclidean_space_iff hom_ee' homeomorphic_maps_def)
-        ultimately show "continuous_on (h ` e ` {- r<..<r}) e'"
-          by (simp add: e'_def continuous_on_subset)
+        then show "continuous_on (h ` e ` {- r<..<r}) e'"
+          using hesub by (simp add: 1 e'_def continuous_on_subset)
       qed
       show "openin euclideanreal (e' ` h ` e ` {- r<..<r})"
         using injective_eq_1d_open_map_UNIV [OF cont] inj by (simp add: image_image is_interval_1)
diff -r 021fb1b01de5 -r 74c75da4cb01 src/HOL/Homology/Simplices.thy
--- a/src/HOL/Homology/Simplices.thy	Tue Jul 11 20:22:08 2023 +0100
+++ b/src/HOL/Homology/Simplices.thy	Wed Jul 12 18:28:11 2023 +0100
@@ -699,7 +699,7 @@
    "\<lbrakk>singular_simplex p X c;
      \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk>
     \<Longrightarrow> simplex_map p f c = simplex_map p g c"
-  by (auto simp: singular_simplex_def simplex_map_def continuous_map_def)
+  by (auto simp: singular_simplex_def simplex_map_def continuous_map_def Pi_iff)
 
 lemma simplex_map_id_gen:
    "\<lbrakk>singular_simplex p X c;
@@ -879,14 +879,14 @@
     have "continuous_map (subtopology (product_topology (\<lambda>n. euclideanreal) UNIV) (standard_simplex p)) X f"
       using \<open>singular_simplex p X f\<close> singular_simplex_def by blast
     then have "\<And>c. c \<notin> standard_simplex p \<or> f c = a"
-      by (simp add: assms continuous_map_def)
+      by (simp add: assms continuous_map_def Pi_iff)
     then show ?thesis
       by (metis (no_types) L extensional_restrict restrict_ext singular_simplex_def)
   qed
 next
   assume ?rhs
   with assms show ?lhs
-    by (auto simp: singular_simplex_def topspace_subtopology)
+    by (auto simp: singular_simplex_def)
 qed
 
 lemma singular_chain_singleton:
diff -r 021fb1b01de5 -r 74c75da4cb01 src/HOL/ROOT
--- a/src/HOL/ROOT	Tue Jul 11 20:22:08 2023 +0100
+++ b/src/HOL/ROOT	Wed Jul 12 18:28:11 2023 +0100
@@ -98,7 +98,7 @@
   document_files "root.bib" "root.tex"
 
 session "HOL-Analysis" (main timing) in Analysis = HOL +
-  options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
+  options [timeout=1800, document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
     document_variants = "document:manual=-proof,-ML,-unimportant"]
   sessions
     "HOL-Library"
@@ -111,7 +111,7 @@
     "root.bib"
 
 session "HOL-Complex_Analysis" (main timing) in Complex_Analysis = "HOL-Analysis" +
-  options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
+  options [timeout=300, document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
     document_variants = "document:manual=-proof,-ML,-unimportant"]
   theories
     Complex_Analysis
@@ -125,7 +125,7 @@
     Metric_Arith_Examples
 
 session "HOL-Homology" (timing) in Homology = "HOL-Analysis" +
-  options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
+  options [timeout=300, document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
     document_variants = "document:manual=-proof,-ML,-unimportant"]
   sessions
     "HOL-Algebra"
@@ -322,6 +322,7 @@
     Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
     Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity.
   "
+  options [timeout = 300]
   sessions
     "HOL-Algebra"
   theories
@@ -846,6 +847,7 @@
     ATP_Problem_Import
 
 session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" +
+  options [timeout = 300]
   sessions
     "HOL-Combinatorics"
   theories