--- 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)
--- 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>
--- 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)
--- 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:
--- 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