--- a/src/HOL/Analysis/Cartesian_Space.thy Fri Aug 04 19:17:49 2023 +0200
+++ b/src/HOL/Analysis/Cartesian_Space.thy Sun Aug 06 18:29:09 2023 +0100
@@ -30,70 +30,66 @@
interpretation vec: vector_space "(*s) "
by unfold_locales (vector algebra_simps)+
-lemma independent_cart_basis:
- "vec.independent (cart_basis)"
+lemma independent_cart_basis: "vec.independent (cart_basis)"
proof (rule vec.independent_if_scalars_zero)
show "finite (cart_basis)" using finite_cart_basis .
fix f::"('a, 'b) vec \<Rightarrow> 'a" and x::"('a, 'b) vec"
assume eq_0: "(\<Sum>x\<in>cart_basis. f x *s x) = 0" and x_in: "x \<in> cart_basis"
obtain i where x: "x = axis i 1" using x_in unfolding cart_basis_def by auto
have sum_eq_0: "(\<Sum>x\<in>(cart_basis) - {x}. f x * (x $ i)) = 0"
- proof (rule sum.neutral, rule ballI)
- fix xa assume xa: "xa \<in> cart_basis - {x}"
- obtain a where a: "xa = axis a 1" and a_not_i: "a \<noteq> i"
- using xa x unfolding cart_basis_def by auto
- have "xa $ i = 0" unfolding a axis_def using a_not_i by auto
- thus "f xa * xa $ i = 0" by simp
+ proof (intro sum.neutral ballI)
+ fix y assume y: "y \<in> cart_basis - {x}"
+ obtain a where a: "y = axis a 1" and a_not_i: "a \<noteq> i"
+ using y x unfolding cart_basis_def by auto
+ have "y $ i = 0" unfolding a axis_def using a_not_i by auto
+ thus "f y * y $ i = 0" by simp
qed
have "0 = (\<Sum>x\<in>cart_basis. f x *s x) $ i" using eq_0 by simp
- also have "... = (\<Sum>x\<in>cart_basis. (f x *s x) $ i)" unfolding sum_component ..
- also have "... = (\<Sum>x\<in>cart_basis. f x * (x $ i))" unfolding vector_smult_component ..
- also have "... = f x * (x $ i) + (\<Sum>x\<in>(cart_basis) - {x}. f x * (x $ i))"
+ also have "\<dots> = (\<Sum>x\<in>cart_basis. (f x *s x) $ i)" unfolding sum_component ..
+ also have "\<dots> = (\<Sum>x\<in>cart_basis. f x * (x $ i))" unfolding vector_smult_component ..
+ also have "\<dots> = f x * (x $ i) + (\<Sum>x\<in>(cart_basis) - {x}. f x * (x $ i))"
by (rule sum.remove[OF finite_cart_basis x_in])
- also have "... = f x * (x $ i)" unfolding sum_eq_0 by simp
- also have "... = f x" unfolding x axis_def by auto
+ also have "\<dots> = f x * (x $ i)" unfolding sum_eq_0 by simp
+ also have "\<dots> = f x" unfolding x axis_def by auto
finally show "f x = 0" ..
qed
-lemma span_cart_basis:
- "vec.span (cart_basis) = UNIV"
-proof (auto)
- fix x::"('a, 'b) vec"
- let ?f="\<lambda>v. x $ (THE i. v = axis i 1)"
- show "x \<in> vec.span (cart_basis)"
- apply (unfold vec.span_finite[OF finite_cart_basis])
- apply (rule image_eqI[of _ _ ?f])
- apply (subst vec_eq_iff)
- apply clarify
+lemma span_cart_basis [simp]: "vec.span (cart_basis) = UNIV"
+proof -
+ have "x \<in> vec.span cart_basis" for x :: "('a, 'b) vec"
proof -
- fix i::'b
- let ?w = "axis i (1::'a)"
- have the_eq_i: "(THE a. ?w = axis a 1) = i"
- by (rule the_equality, auto simp: axis_eq_axis)
- have sum_eq_0: "(\<Sum>v\<in>(cart_basis) - {?w}. x $ (THE i. v = axis i 1) * v $ i) = 0"
- proof (rule sum.neutral, rule ballI)
- fix xa::"('a, 'b) vec"
- assume xa: "xa \<in> cart_basis - {?w}"
- obtain j where j: "xa = axis j 1" and i_not_j: "i \<noteq> j" using xa unfolding cart_basis_def by auto
- have the_eq_j: "(THE i. xa = axis i 1) = j"
- proof (rule the_equality)
- show "xa = axis j 1" using j .
- show "\<And>i. xa = axis i 1 \<Longrightarrow> i = j" by (metis axis_eq_axis j zero_neq_one)
+ let ?f="\<lambda>v. x $ (THE i. v = axis i 1)"
+ have "x $ i = (\<Sum>v\<in>cart_basis. x $ (THE i. v = axis i 1) *s v) $ i" for i::'b
+ proof -
+ let ?w = "axis i (1::'a)"
+ have the_eq_i: "(THE a. ?w = axis a 1) = i"
+ by (rule the_equality, auto simp: axis_eq_axis)
+ have sum_eq_0: "(\<Sum>v\<in>(cart_basis) - {?w}. x $ (THE i. v = axis i 1) * v $ i) = 0"
+ proof (intro sum.neutral ballI)
+ fix y:: "('a, 'b) vec"
+ assume y: "y \<in> cart_basis - {?w}"
+ obtain j where j: "y = axis j 1" and i_not_j: "i \<noteq> j"
+ using y unfolding cart_basis_def by auto
+ have the_eq_j: "(THE i. y = axis i 1) = j"
+ by (simp add: axis_eq_axis j)
+ show "x $ (THE i. y = axis i 1) * y $ i = 0"
+ by (simp add: axis_def i_not_j j)
qed
- show "x $ (THE i. xa = axis i 1) * xa $ i = 0"
- apply (subst (2) j)
- unfolding the_eq_j unfolding axis_def using i_not_j by simp
+ have "(\<Sum>v\<in>cart_basis. x $ (THE i. v = axis i 1) *s v) $ i
+ = (\<Sum>v\<in>cart_basis. x $ (THE i. v = axis i 1) * v $ i)"
+ by force
+ also have "\<dots> = x $ (THE a. ?w = axis a 1) * ?w $ i + (\<Sum>v\<in>(cart_basis) - {?w}. x $ (THE i. v = axis i 1) * v $ i)"
+ by (rule sum.remove[OF finite_cart_basis], auto simp add: cart_basis_def)
+ also have "\<dots> = x $ (THE a. ?w = axis a 1) * ?w $ i"
+ unfolding sum_eq_0 by simp
+ also have "\<dots> = x $ i"
+ unfolding the_eq_i unfolding axis_def by auto
+ finally show ?thesis by simp
qed
- have "(\<Sum>v\<in>cart_basis. x $ (THE i. v = axis i 1) *s v) $ i =
- (\<Sum>v\<in>cart_basis. (x $ (THE i. v = axis i 1) *s v) $ i)" unfolding sum_component ..
- also have "... = (\<Sum>v\<in>cart_basis. x $ (THE i. v = axis i 1) * v $ i)"
- unfolding vector_smult_component ..
- also have "... = x $ (THE a. ?w = axis a 1) * ?w $ i + (\<Sum>v\<in>(cart_basis) - {?w}. x $ (THE i. v = axis i 1) * v $ i)"
- by (rule sum.remove[OF finite_cart_basis], auto simp add: cart_basis_def)
- also have "... = x $ (THE a. ?w = axis a 1) * ?w $ i" unfolding sum_eq_0 by simp
- also have "... = x $ i" unfolding the_eq_i unfolding axis_def by auto
- finally show "x $ i = (\<Sum>v\<in>cart_basis. x $ (THE i. v = axis i 1) *s v) $ i" by simp
- qed simp
+ then show "x \<in> vec.span (cart_basis)"
+ by (metis (no_types, lifting) vec.span_base vec.span_scale vec.span_sum vec_eq_iff)
+ qed
+ then show ?thesis by auto
qed
(*Some interpretations:*)
@@ -138,10 +134,12 @@
lemma matrix_works:
assumes lf: "Vector_Spaces.linear (*s) (*s) f"
shows "matrix f *v x = f (x::'a::field ^ 'n)"
- apply (simp add: matrix_def matrix_vector_mult_def vec_eq_iff mult.commute)
- apply clarify
- apply (rule linear_componentwise[OF lf, symmetric])
- done
+proof -
+ have "\<forall>i. (\<Sum>j\<in>UNIV. x $ j * f (axis j 1) $ i) = f x $ i"
+ by (simp add: Cartesian_Space.linear_componentwise lf)
+ then show ?thesis
+ by (simp add: matrix_def matrix_vector_mult_def vec_eq_iff mult.commute)
+qed
lemma matrix_of_matrix_vector_mul[simp]: "matrix(\<lambda>x. A *v (x :: 'a::field ^ 'n)) = A"
by (simp add: matrix_eq matrix_works)
@@ -190,44 +188,27 @@
next
assume "inj ((*v) A)"
from vec.linear_injective_left_inverse[OF matrix_vector_mul_linear_gen this]
- obtain g where "Vector_Spaces.linear (*s) (*s) g" and g: "g \<circ> (*v) A = id"
+ obtain g where "Vector_Spaces.linear (*s) (*s) g" and "g \<circ> (*v) A = id"
by blast
- have "matrix g ** A = mat 1"
- by (metis matrix_vector_mul_linear_gen \<open>Vector_Spaces.linear (*s) (*s) g\<close> g matrix_compose_gen
- matrix_eq matrix_id_mat_1 matrix_vector_mul(1))
+ then have "matrix g ** A = mat 1"
+ by (metis matrix_compose_gen matrix_id_mat_1 matrix_of_matrix_vector_mul vec.linear_axioms)
then show "\<exists>B. B ** A = mat 1"
by metis
qed
lemma matrix_left_invertible_ker:
"(\<exists>B. (B::'a::{field} ^'m^'n) ** (A::'a::{field}^'n^'m) = mat 1) \<longleftrightarrow> (\<forall>x. A *v x = 0 \<longrightarrow> x = 0)"
- unfolding matrix_left_invertible_injective
- using vec.inj_on_iff_eq_0[OF vec.subspace_UNIV, of A]
- by (simp add: inj_on_def)
+ by (simp add: matrix_left_invertible_injective vec.inj_iff_eq_0)
lemma matrix_right_invertible_surjective:
"(\<exists>B. (A::'a::field^'n^'m) ** (B::'a::field^'m^'n) = mat 1) \<longleftrightarrow> surj (\<lambda>x. A *v x)"
proof -
- { fix B :: "'a ^'m^'n"
- assume AB: "A ** B = mat 1"
- { fix x :: "'a ^ 'm"
- have "A *v (B *v x) = x"
- by (simp add: matrix_vector_mul_assoc AB) }
- hence "surj ((*v) A)" unfolding surj_def by metis }
- moreover
- { assume sf: "surj ((*v) A)"
- from vec.linear_surjective_right_inverse[OF _ this]
- obtain g:: "'a ^'m \<Rightarrow> 'a ^'n" where g: "Vector_Spaces.linear (*s) (*s) g" "(*v) A \<circ> g = id"
- by blast
-
- have "A ** (matrix g) = mat 1"
- unfolding matrix_eq matrix_vector_mul_lid
- matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)]
- using g(2) unfolding o_def fun_eq_iff id_def
- .
- hence "\<exists>B. A ** (B::'a^'m^'n) = mat 1" by blast
- }
- ultimately show ?thesis unfolding surj_def by blast
+ have "\<And>B x. A ** B = mat 1 \<Longrightarrow> \<exists>y. x = A *v y"
+ by (metis matrix_vector_mul_assoc matrix_vector_mul_lid)
+ moreover have "\<forall>x. \<exists>xa. x = A *v xa \<Longrightarrow> \<exists>B. A ** B = mat 1"
+ by (metis (mono_tags, lifting) matrix_compose_gen matrix_id_mat_1 matrix_of_matrix_vector_mul surj_def vec.linear_axioms vec.linear_surjective_right_inverse)
+ ultimately show ?thesis
+ by (auto simp: image_def set_eq_iff)
qed
lemma matrix_left_invertible_independent_columns:
@@ -237,33 +218,20 @@
(is "?lhs \<longleftrightarrow> ?rhs")
proof -
let ?U = "UNIV :: 'n set"
- { assume k: "\<forall>x. A *v x = 0 \<longrightarrow> x = 0"
- { fix c i
- assume c: "sum (\<lambda>i. c i *s column i A) ?U = 0" and i: "i \<in> ?U"
- let ?x = "\<chi> i. c i"
- have th0:"A *v ?x = 0"
- using c
- by (vector matrix_mult_sum)
- from k[rule_format, OF th0] i
- have "c i = 0" by (vector vec_eq_iff)}
- hence ?rhs by blast }
- moreover
- { assume H: ?rhs
- { fix x assume x: "A *v x = 0"
- let ?c = "\<lambda>i. ((x$i ):: 'a)"
- from H[rule_format, of ?c, unfolded matrix_mult_sum[symmetric], OF x]
- have "x = 0" by vector }
- }
- ultimately show ?thesis unfolding matrix_left_invertible_ker by auto
+ have "c i = 0"
+ if "\<forall>x. A *v x = 0 \<longrightarrow> x = 0" "sum (\<lambda>i. c i *s column i A) ?U = 0" for c i
+ by (metis (no_types) UNIV_I matrix_mult_sum vec_lambda_eta vec_nth_cases zero_vec_def that)
+ moreover have "x = 0" if "A *v x = 0" ?rhs for x
+ by (metis (full_types) matrix_mult_sum that vec_eq_iff zero_index)
+ ultimately show ?thesis
+ unfolding matrix_left_invertible_ker by auto
qed
lemma matrix_right_invertible_independent_rows:
fixes A :: "'a::{field}^'n^'m"
shows "(\<exists>(B::'a^'m^'n). A ** B = mat 1) \<longleftrightarrow>
- (\<forall>c. sum (\<lambda>i. c i *s row i A) (UNIV :: 'm set) = 0 \<longrightarrow> (\<forall>i. c i = 0))"
- unfolding left_invertible_transpose[symmetric]
- matrix_left_invertible_independent_columns
- by (simp add:)
+ (\<forall>c. sum (\<lambda>i::'m. c i *s row i A) UNIV = 0 \<longrightarrow> (\<forall>i. c i = 0))"
+ by (simp add: matrix_left_invertible_independent_columns flip: left_invertible_transpose)
lemma matrix_right_invertible_span_columns:
"(\<exists>(B::'a::field ^'n^'m). (A::'a ^'m^'n) ** B = mat 1) \<longleftrightarrow>
@@ -277,14 +245,10 @@
have rhseq: "?rhs \<longleftrightarrow> (\<forall>x. x \<in> vec.span (columns A))" by blast
{ assume h: ?lhs
{ fix x:: "'a ^'n"
- from h[unfolded lhseq, rule_format, of x] obtain y :: "'a ^'m"
- where y: "sum (\<lambda>i. (y$i) *s column i A) ?U = x" by blast
- have "x \<in> vec.span (columns A)"
- unfolding y[symmetric] scalar_mult_eq_scaleR
- proof (rule vec.span_sum [OF vec.span_scale])
- show "column i A \<in> vec.span (columns A)" for i
- using columns_def vec.span_superset by auto
- qed
+ obtain y :: "'a ^'m" where y: "sum (\<lambda>i. (y$i) *s column i A) ?U = x"
+ using h lhseq by blast
+ then have "x \<in> vec.span (columns A)"
+ by (metis (mono_tags, lifting) columns_def mem_Collect_eq vec.span_base vec.span_scale vec.span_sum)
}
then have ?rhs unfolding rhseq by blast }
moreover
@@ -313,14 +277,14 @@
using i(1) by (simp add: field_simps)
have "sum (\<lambda>xa. if xa = i then (c + (x$i)) * ((column xa A)$j)
else (x$xa) * ((column xa A$j))) ?U = sum (\<lambda>xa. (if xa = i then c * ((column i A)$j) else 0) + ((x$xa) * ((column xa A)$j))) ?U"
- by (rule sum.cong[OF refl]) (use th in blast)
+ using th by force
also have "\<dots> = sum (\<lambda>xa. if xa = i then c * ((column i A)$j) else 0) ?U + sum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U"
by (simp add: sum.distrib)
also have "\<dots> = c * ((column i A)$j) + sum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U"
- unfolding sum.delta[OF fU]
- using i(1) by simp
+ unfolding sum.delta[OF fU] using i(1) by simp
finally show "sum (\<lambda>xa. if xa = i then (c + (x$i)) * ((column xa A)$j)
- else (x$xa) * ((column xa A$j))) ?U = c * ((column i A)$j) + sum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U" .
+ else (x$xa) * ((column xa A$j))) ?U
+ = c * ((column i A)$j) + sum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U" .
qed
qed
}
@@ -331,10 +295,7 @@
lemma matrix_left_invertible_span_rows_gen:
"(\<exists>(B::'a^'m^'n). B ** (A::'a::field^'n^'m) = mat 1) \<longleftrightarrow> vec.span (rows A) = UNIV"
- unfolding right_invertible_transpose[symmetric]
- unfolding columns_transpose[symmetric]
- unfolding matrix_right_invertible_span_columns
- ..
+ by (metis columns_transpose matrix_right_invertible_span_columns right_invertible_transpose)
lemma matrix_left_invertible_span_rows:
"(\<exists>(B::real^'m^'n). B ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> span (rows A) = UNIV"
@@ -348,17 +309,13 @@
assume AA': "A ** A' = mat 1"
have sA: "surj ((*v) A)"
using AA' matrix_right_invertible_surjective by auto
- from vec.linear_surjective_isomorphism[OF matrix_vector_mul_linear_gen sA]
obtain f' :: "'a ^'n \<Rightarrow> 'a ^'n"
- where f': "Vector_Spaces.linear (*s) (*s) f'" "\<forall>x. f' (A *v x) = x" "\<forall>x. A *v f' x = x" by blast
- have th: "matrix f' ** A = mat 1"
- by (simp add: matrix_eq matrix_works[OF f'(1)]
- matrix_vector_mul_assoc[symmetric] f'(2)[rule_format])
- hence "(matrix f' ** A) ** A' = mat 1 ** A'" by simp
- hence "matrix f' = A'"
- by (simp add: matrix_mul_assoc[symmetric] AA')
- hence "matrix f' ** A = A' ** A" by simp
- hence "A' ** A = mat 1" by (simp add: th)
+ where f': "Vector_Spaces.linear (*s) (*s) f'" "\<forall>x. f' (A *v x) = x" "\<forall>x. A *v f' x = x"
+ using sA vec.linear_surjective_isomorphism by blast
+ have "matrix f' ** A = mat 1"
+ by (metis f' matrix_eq matrix_vector_mul_assoc matrix_vector_mul_lid matrix_works)
+ hence "A' ** A = mat 1"
+ by (metis AA' matrix_mul_assoc matrix_mul_lid)
}
then show ?thesis by blast
qed
@@ -382,22 +339,12 @@
using inv_A unfolding invertible_def by blast
obtain B' where BB': "B ** B' = mat 1" and B'B: "B' ** B = mat 1"
using inv_B unfolding invertible_def by blast
- show ?thesis
- proof (unfold invertible_def, rule exI[of _ "B'**A'"], rule conjI)
- have "A ** B ** (B' ** A') = A ** (B ** (B' ** A'))"
- using matrix_mul_assoc[of A B "(B' ** A')", symmetric] .
- also have "... = A ** (B ** B' ** A')" unfolding matrix_mul_assoc[of B "B'" "A'"] ..
- also have "... = A ** (mat 1 ** A')" unfolding BB' ..
- also have "... = A ** A'" unfolding matrix_mul_lid ..
- also have "... = mat 1" unfolding AA' ..
- finally show "A ** B ** (B' ** A') = mat (1::'a)" .
- have "B' ** A' ** (A ** B) = B' ** (A' ** (A ** B))" using matrix_mul_assoc[of B' A' "(A ** B)", symmetric] .
- also have "... = B' ** (A' ** A ** B)" unfolding matrix_mul_assoc[of A' A B] ..
- also have "... = B' ** (mat 1 ** B)" unfolding A'A ..
- also have "... = B' ** B" unfolding matrix_mul_lid ..
- also have "... = mat 1" unfolding B'B ..
- finally show "B' ** A' ** (A ** B) = mat 1" .
- qed
+ have "A ** B ** (B' ** A') = mat 1"
+ by (metis AA' BB' matrix_mul_assoc matrix_mul_rid)
+ moreover have "B' ** A' ** (A ** B) = mat 1"
+ by (metis A'A B'B matrix_mul_assoc matrix_mul_rid)
+ ultimately show ?thesis
+ using invertible_def by blast
qed
lemma transpose_invertible:
@@ -409,12 +356,7 @@
lemma vector_matrix_mul_assoc:
fixes v :: "('a::comm_semiring_1)^'n"
shows "(v v* M) v* N = v v* (M ** N)"
-proof -
- from matrix_vector_mul_assoc
- have "transpose N *v (transpose M *v v) = (transpose N ** transpose M) *v v" by fast
- thus "(v v* M) v* N = v v* (M ** N)"
- by (simp add: matrix_transpose_mul [symmetric])
-qed
+ by (metis (no_types, opaque_lifting) matrix_transpose_mul matrix_vector_mul_assoc transpose_matrix_vector)
lemma matrix_scaleR_vector_ac:
fixes A :: "real^('m::finite)^'n"
@@ -426,8 +368,7 @@
shows "k *\<^sub>R (A *v v) = k *\<^sub>R A *v v"
by (metis matrix_scaleR_vector_ac matrix_vector_mult_scaleR)
-(*Finally, some interesting theorems and interpretations that don't appear in any file of the
- library.*)
+subsection \<open>Some interesting theorems and interpretations\<close>
locale linear_first_finite_dimensional_vector_space =
l?: Vector_Spaces.linear scaleB scaleC f +
@@ -438,25 +379,10 @@
and f :: "('b=>'c)"
lemma vec_dim_card: "vec.dim (UNIV::('a::{field}^'n) set) = CARD ('n)"
-proof -
- let ?f="\<lambda>i::'n. axis i (1::'a)"
- have "vec.dim (UNIV::('a::{field}^'n) set) = card (cart_basis::('a^'n) set)"
- unfolding vec.dim_UNIV ..
- also have "... = card ({i. i\<in> UNIV}::('n) set)"
- proof (rule bij_betw_same_card[of ?f, symmetric], unfold bij_betw_def, auto)
- show "inj (\<lambda>i::'n. axis i (1::'a))" by (simp add: inj_on_def axis_eq_axis)
- fix i::'n
- show "axis i 1 \<in> cart_basis" unfolding cart_basis_def by auto
- fix x::"'a^'n"
- assume "x \<in> cart_basis"
- thus "x \<in> range (\<lambda>i. axis i 1)" unfolding cart_basis_def by auto
- qed
- also have "... = CARD('n)" by auto
- finally show ?thesis .
-qed
+ by (simp add: card_cart_basis)
interpretation vector_space_over_itself: vector_space "(*) :: 'a::field \<Rightarrow> 'a \<Rightarrow> 'a"
-by unfold_locales (simp_all add: algebra_simps)
+ by unfold_locales (simp_all add: algebra_simps)
lemmas [simp del] = vector_space_over_itself.scale_scale
@@ -484,24 +410,12 @@
by (simp add: matrix_vector_mult_def inner_vec_def)
lemma adjoint_matrix: "adjoint(\<lambda>x. (A::real^'n^'m) *v x) = (\<lambda>x. transpose A *v x)"
- apply (rule adjoint_unique)
- apply (simp add: transpose_def inner_vec_def matrix_vector_mult_def
- sum_distrib_right sum_distrib_left)
- apply (subst sum.swap)
- apply (simp add: ac_simps)
- done
+ by (metis adjoint_unique dot_lmul_matrix vector_transpose_matrix)
-lemma matrix_adjoint: assumes lf: "linear (f :: real^'n \<Rightarrow> real ^'m)"
+lemma matrix_adjoint:
+ assumes lf: "linear (f :: real^'n \<Rightarrow> real ^'m)"
shows "matrix(adjoint f) = transpose(matrix f)"
-proof -
- have "matrix(adjoint f) = matrix(adjoint ((*v) (matrix f)))"
- by (simp add: lf)
- also have "\<dots> = transpose(matrix f)"
- unfolding adjoint_matrix matrix_of_matrix_vector_mul
- apply rule
- done
- finally show ?thesis .
-qed
+ by (metis adjoint_matrix assms matrix_of_matrix_vector_mul matrix_vector_mul(2))
subsection\<open> Rank of a matrix\<close>
@@ -511,10 +425,8 @@
lemma matrix_vector_mult_in_columnspace_gen:
fixes A :: "'a::field^'n^'m"
shows "(A *v x) \<in> vec.span(columns A)"
- apply (simp add: matrix_vector_column columns_def transpose_def column_def)
- apply (intro vec.span_sum vec.span_scale)
- apply (force intro: vec.span_base)
- done
+ unfolding columns_def
+ by (metis (mono_tags, lifting) matrix_mult_sum mem_Collect_eq vec.span_base vec.span_scale vec.span_sum)
lemma matrix_vector_mult_in_columnspace:
fixes A :: "real^'n^'m"
@@ -576,9 +488,7 @@
then have ind: "independent ((*v) A ` B)"
by (rule linear_independent_injective_image [OF Finite_Cartesian_Product.matrix_vector_mul_linear \<open>independent B\<close>])
have "dim (span (rows A)) \<le> card ((*v) A ` B)"
- unfolding B(2)[symmetric]
- using inj
- by (auto simp: card_image inj_on_subset span_superset)
+ by (metis B(2) card_image inj inj_on_subset order.refl span_superset)
also have "\<dots> \<le> dim (span (columns A))"
using _ ind
by (rule independent_card_le_dim) (auto intro!: matrix_vector_mult_in_columnspace)
@@ -613,13 +523,7 @@
fixes A :: "real^'n^'m"
shows "rank A = dim(range (\<lambda>x. A *v x))"
unfolding column_rank_def
-proof (rule span_eq_dim)
- have "span (columns A) \<subseteq> span (range ((*v) A))" (is "?l \<subseteq> ?r")
- by (simp add: columns_image_basis image_subsetI span_mono)
- then show "?l = ?r"
- by (metis (no_types, lifting) image_subset_iff matrix_vector_mult_in_columnspace
- span_eq span_span)
-qed
+ by (smt (verit, best) columns_image_basis dim_span image_subset_iff iso_tuple_UNIV_I matrix_vector_mult_in_columnspace span_eq)
lemma rank_bound:
fixes A :: "real^'n^'m"
@@ -636,8 +540,7 @@
lemma full_rank_surjective:
fixes A :: "real^'n^'m"
shows "rank A = CARD('m) \<longleftrightarrow> surj ((*v) A)"
- by (simp add: matrix_right_invertible_surjective [symmetric] left_invertible_transpose [symmetric]
- matrix_left_invertible_injective full_rank_injective [symmetric] rank_transpose)
+ by (metis (no_types, opaque_lifting) dim_eq_full dim_vec_eq rank_dim_range span_vec_eq vec.span_UNIV vec.span_image vec_dim_card)
lemma rank_I: "rank(mat 1::real^'n^'n) = CARD('n)"
by (simp add: full_rank_injective inj_on_def)
@@ -645,7 +548,7 @@
lemma less_rank_noninjective:
fixes A :: "real^'n^'m"
shows "rank A < CARD('n) \<longleftrightarrow> \<not> inj ((*v) A)"
-using less_le rank_bound by (auto simp: full_rank_injective [symmetric])
+ using less_le rank_bound by (auto simp: full_rank_injective [symmetric])
lemma matrix_nonfull_linear_equations_eq:
fixes A :: "real^'n^'m"
@@ -680,9 +583,10 @@
shows "x = 1 \<or> x = 2"
proof (induct x)
case (of_int z)
- then have "0 \<le> z" and "z < 2" by simp_all
- then have "z = 0 | z = 1" by arith
- then show ?case by auto
+ then have "z = 0 | z = 1"
+ by fastforce
+ then show ?case
+ by auto
qed
lemma forall_2: "(\<forall>i::2. P i) \<longleftrightarrow> P 1 \<and> P 2"
@@ -693,8 +597,7 @@
shows "x = 1 \<or> x = 2 \<or> x = 3"
proof (induct x)
case (of_int z)
- then have "0 \<le> z" and "z < 3" by simp_all
- then have "z = 0 \<or> z = 1 \<or> z = 2" by arith
+ then have "z = 0 \<or> z = 1 \<or> z = 2" by fastforce
then show ?case by auto
qed
@@ -706,8 +609,7 @@
shows "x = 1 \<or> x = 2 \<or> x = 3 \<or> x = 4"
proof (induct x)
case (of_int z)
- then have "0 \<le> z" and "z < 4" by simp_all
- then have "z = 0 \<or> z = 1 \<or> z = 2 \<or> z = 3" by arith
+ then have "z = 0 \<or> z = 1 \<or> z = 2 \<or> z = 3" by fastforce
then show ?case by auto
qed
@@ -744,10 +646,7 @@
by (simp add: vec_eq_iff)
lemma forall_one: "(\<forall>(x::'a ^1). P x) \<longleftrightarrow> (\<forall>x. P(\<chi> i. x))"
- apply auto
- apply (erule_tac x= "x$1" in allE)
- apply (simp only: vector_one[symmetric])
- done
+ by (metis vector_one)
lemma norm_vector_1: "norm (x :: _^1) = norm (x$1)"
by (simp add: norm_vec_def)
@@ -791,7 +690,7 @@
shows "((\<lambda>x. vec (g (x $ 1))) has_derivative (*\<^sub>R) (g' a))
(at ((vec a)::real^1) within vec ` S)"
using der_g
- apply (auto simp: Deriv.has_derivative_within bounded_linear_scaleR_right norm_vector_1)
+ apply (clarsimp simp: Deriv.has_derivative_within bounded_linear_scaleR_right norm_vector_1)
apply (drule tendsto_at_within_vector_1, vector)
apply (auto simp: algebra_simps eventually_at tendsto_def)
done
@@ -817,46 +716,33 @@
by (metis vector_1 vector_one)
lemma forall_vector_2: "(\<forall>v::'a::zero^2. P v) \<longleftrightarrow> (\<forall>x y. P(vector[x, y]))"
- apply auto
- apply (erule_tac x="v$1" in allE)
- apply (erule_tac x="v$2" in allE)
- apply (subgoal_tac "vector [v$1, v$2] = v")
- apply simp
- apply (vector vector_def)
- apply (simp add: forall_2)
- done
+proof -
+ have "P v" if "\<And>x y. P (vector [x, y])" for v
+ proof -
+ have "vector [v$1, v$2] = v"
+ by (smt (verit, best) exhaust_2 vec_eq_iff vector_2)
+ then show ?thesis
+ by (metis that)
+ qed
+ then show ?thesis by auto
+qed
lemma forall_vector_3: "(\<forall>v::'a::zero^3. P v) \<longleftrightarrow> (\<forall>x y z. P(vector[x, y, z]))"
- apply auto
- apply (erule_tac x="v$1" in allE)
- apply (erule_tac x="v$2" in allE)
- apply (erule_tac x="v$3" in allE)
- apply (subgoal_tac "vector [v$1, v$2, v$3] = v")
- apply simp
- apply (vector vector_def)
- apply (simp add: forall_3)
- done
+proof -
+ have "P v" if "\<And>x y z. P (vector [x, y, z])" for v
+ proof -
+ have "vector [v$1, v$2, v$3] = v"
+ by (smt (verit, best) exhaust_3 vec_eq_iff vector_3)
+ then show ?thesis
+ by (metis that)
+ qed
+ then show ?thesis by auto
+qed
subsection\<^marker>\<open>tag unimportant\<close> \<open>lambda skolemization on cartesian products\<close>
-lemma lambda_skolem: "(\<forall>i. \<exists>x. P i x) \<longleftrightarrow>
- (\<exists>x::'a ^ 'n. \<forall>i. P i (x $ i))" (is "?lhs \<longleftrightarrow> ?rhs")
-proof -
- let ?S = "(UNIV :: 'n set)"
- { assume H: "?rhs"
- then have ?lhs by auto }
- moreover
- { assume H: "?lhs"
- then obtain f where f:"\<forall>i. P i (f i)" unfolding choice_iff by metis
- let ?x = "(\<chi> i. (f i)) :: 'a ^ 'n"
- { fix i
- from f have "P i (f i)" by metis
- then have "P i (?x $ i)" by auto
- }
- hence "\<forall>i. P i (?x$i)" by metis
- hence ?rhs by metis }
- ultimately show ?thesis by metis
-qed
+lemma lambda_skolem: "(\<forall>i. \<exists>x. P i x) \<longleftrightarrow> (\<exists>x::'a ^ 'n. \<forall>i. P i (x $ i))"
+ by (metis vec_lambda_beta)
text \<open>The same result in terms of square matrices.\<close>
@@ -885,8 +771,7 @@
fixes A B :: "real ^'n ^'n" and x y :: "real ^'n"
shows "(A *v x) \<bullet> (B *v y) =
(((rowvector x :: real^'n^1) ** ((transpose A ** B) ** (columnvector y :: real ^1^'n)))$1)$1"
- unfolding dot_matrix_product transpose_columnvector[symmetric]
- dot_rowvector_columnvector matrix_transpose_mul matrix_mul_assoc ..
+ by (metis dot_lmul_matrix dot_matrix_product dot_rowvector_columnvector matrix_mul_assoc vector_transpose_matrix)
lemma dim_substandard_cart: "vec.dim {x::'a::field^'n. \<forall>i. i \<notin> d \<longrightarrow> x$i = 0} = card d"
@@ -931,7 +816,7 @@
hence "m *s x = y - c" by (simp add: field_simps)
hence "inverse m *s (m *s x) = inverse m *s (y - c)" by simp
then show "x = inverse m *s y + - (inverse m *s c)"
- using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib)
+ by (simp add: m0 vec.scale_right_diff_distrib)
next
assume h: "x = inverse m *s y + - (inverse m *s c)"
show "m *s x + c = y" unfolding h
@@ -940,8 +825,7 @@
lemma vector_eq_affinity:
"(m::'a::field) \<noteq> 0 ==> (y = m *s x + c \<longleftrightarrow> inverse(m) *s y + -(inverse(m) *s c) = x)"
- using vector_affinity_eq[where m=m and x=x and y=y and c=c]
- by metis
+ by (metis vector_affinity_eq)
lemma vector_cart:
fixes f :: "real^'n \<Rightarrow> real"
@@ -1017,14 +901,9 @@
by blast
}
moreover
- {
- assume lf: "Vector_Spaces.linear (*s) (*s) f" and om: "orthogonal_matrix ?mf"
- from lf om have ?lhs
- unfolding orthogonal_matrix_def norm_eq orthogonal_transformation
- apply (simp only: matrix_works[OF lf, symmetric] dot_matrix_vector_mul)
- apply (simp add: dot_matrix_product linear_def scalar_mult_eq_scaleR)
- done
- }
+ have ?lhs if "Vector_Spaces.linear (*s) (*s) f" and "orthogonal_matrix ?mf"
+ using that unfolding orthogonal_matrix_def norm_eq orthogonal_transformation
+ by (metis dot_matrix_product dot_matrix_vector_mul linear_matrix_vector_mul_eq matrix_mul_lid matrix_vector_mul(2))
ultimately show ?thesis
by (auto simp: linear_def scalar_mult_eq_scaleR)
qed
@@ -1052,7 +931,7 @@
(\<forall>i j. i \<noteq> j \<longrightarrow> orthogonal (row i A) (row j A))"
using orthogonal_matrix_orthonormal_columns [of "transpose A"] by simp
-proposition orthogonal_matrix_exists_basis:
+proposition orthogonal_matrix_exists_basis:
fixes a :: "real^'n"
assumes "norm a = 1"
obtains A where "orthogonal_matrix A" "A *v (axis k 1) = a"
@@ -1084,16 +963,13 @@
assumes "norm a = 1" "norm b = 1"
obtains f where "orthogonal_transformation f" "f a = b"
proof -
- obtain k::'n where True
- by simp
- obtain A B where AB: "orthogonal_matrix A" "orthogonal_matrix B" and eq: "A *v (axis k 1) = a" "B *v (axis k 1) = b"
+ obtain k A B where AB: "orthogonal_matrix A" "orthogonal_matrix B" and eq: "A *v (axis k 1) = a" "B *v (axis k 1) = b"
using orthogonal_matrix_exists_basis assms by metis
let ?f = "\<lambda>x. (B ** transpose A) *v x"
show thesis
proof
show "orthogonal_transformation ?f"
- by (subst orthogonal_transformation_matrix)
- (auto simp: AB orthogonal_matrix_mul)
+ by (simp add: AB orthogonal_matrix_mul orthogonal_transformation_matrix)
next
show "?f a = b"
using \<open>orthogonal_matrix A\<close> unfolding orthogonal_matrix_def
@@ -1101,7 +977,7 @@
qed
qed
-proposition orthogonal_transformation_exists:
+proposition orthogonal_transformation_exists:
fixes a b :: "real^'n"
assumes "norm a = norm b"
obtains f where "orthogonal_transformation f" "f a = b"
@@ -1114,16 +990,7 @@
then obtain f where f: "orthogonal_transformation f" and eq: "f (a /\<^sub>R norm a) = (b /\<^sub>R norm b)"
by (auto intro: orthogonal_transformation_exists_1 [of "a /\<^sub>R norm a" "b /\<^sub>R norm b"])
show ?thesis
- proof
- interpret linear f
- using f by (simp add: orthogonal_transformation_linear)
- have "f a /\<^sub>R norm a = f (a /\<^sub>R norm a)"
- by (simp add: scale)
- also have "\<dots> = b /\<^sub>R norm a"
- by (simp add: eq assms [symmetric])
- finally show "f a = b"
- using False by auto
- qed (use f in auto)
+ using False assms eq f orthogonal_transformation_scaleR that by fastforce
qed
@@ -1157,9 +1024,7 @@
proposition orthogonal_transformation_isometry:
"orthogonal_transformation f \<longleftrightarrow> f(0::'a::real_inner) = (0::'a) \<and> (\<forall>x y. dist(f x) (f y) = dist x y)"
unfolding orthogonal_transformation
- apply (auto simp: linear_0 isometry_linear)
- apply (metis (no_types, opaque_lifting) dist_norm linear_diff)
- by (metis dist_0_norm)
+ by (metis dist_0_norm dist_norm isometry_linear linear_0 linear_diff)
text \<open>Can extend an isometry from unit sphere:\<close>
@@ -1369,10 +1234,7 @@
apply (simp add: if_if_eq_conj sum.neutral conj_commute cong: conj_cong)
done
show ?thesis
- apply (subst eq)
- apply (intro mult idplus that)
- apply (auto intro: diagonal)
- done
+ unfolding eq by (intro mult idplus that) (auto intro: diagonal)
qed
show ?thesis
by (rule induct_matrix_elementary) (auto intro: assms *)
--- a/src/HOL/Analysis/Interval_Integral.thy Fri Aug 04 19:17:49 2023 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy Sun Aug 06 18:29:09 2023 +0100
@@ -115,7 +115,6 @@
"\<And>i. ereal (l i) < c"
"(\<lambda>x. ereal (l x)) \<longlonglongrightarrow> a"
by auto
- { fix i from less_trans[OF \<open>l i < c\<close> \<open>c < u i\<close>] have "l i < u i" by simp }
have "einterval a b = (\<Union>i. {l i .. u i})"
proof (auto simp: einterval_iff)
fix x assume "a < ereal x" "ereal x < b"
@@ -134,8 +133,9 @@
show "a < ereal x" "ereal x < b"
by (auto simp flip: ereal_less_eq(3))
qed
- show thesis
- by (intro that) fact+
+ moreover { fix i from less_trans[OF \<open>l i < c\<close> \<open>c < u i\<close>] have "l i < u i" by simp }
+ ultimately show thesis
+ by (simp add: l that u)
qed
(* TODO: in this definition, it would be more natural if einterval a b included a and b when
@@ -191,9 +191,9 @@
lemma interval_lebesgue_integral_add [intro, simp]:
fixes M a b f
assumes "interval_lebesgue_integrable M a b f" "interval_lebesgue_integrable M a b g"
- shows "interval_lebesgue_integrable M a b (\<lambda>x. f x + g x)" and
- "interval_lebesgue_integral M a b (\<lambda>x. f x + g x) =
- interval_lebesgue_integral M a b f + interval_lebesgue_integral M a b g"
+ shows "interval_lebesgue_integrable M a b (\<lambda>x. f x + g x)"
+ and "interval_lebesgue_integral M a b (\<lambda>x. f x + g x) =
+ interval_lebesgue_integral M a b f + interval_lebesgue_integral M a b g"
using assms by (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def
field_simps)
@@ -291,11 +291,8 @@
next
case (le a b)
have "LBINT x:{x. - x \<in> einterval a b}. f (- x) = LBINT x:einterval (- b) (- a). f (- x)"
- unfolding interval_lebesgue_integrable_def set_lebesgue_integral_def
- apply (rule Bochner_Integration.integral_cong [OF refl])
- by (auto simp: einterval_iff ereal_uminus_le_reorder ereal_uminus_less_reorder not_less
- simp flip: uminus_ereal.simps
- split: split_indicator)
+ unfolding interval_lebesgue_integrable_def set_lebesgue_integral_def einterval_def
+ by (metis (lifting) ereal_less_uminus_reorder ereal_uminus_less_reorder indicator_simps mem_Collect_eq uminus_ereal.simps(1))
then show ?case
unfolding interval_lebesgue_integral_def
by (subst set_integral_reflect) (simp add: le)
@@ -333,27 +330,12 @@
assumes "AE x \<in> einterval (min a b) (max a b) in lborel. f x = g x"
shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g"
using assms
-proof (induct a b rule: linorder_wlog)
- case (sym a b) then show ?case
- by (simp add: min.commute max.commute interval_integral_endpoints_reverse[of a b])
-next
- case (le a b) then show ?case
- by (auto simp: interval_lebesgue_integral_def max_def min_def
- intro!: set_lebesgue_integral_cong_AE)
-qed
+ by (auto simp: interval_lebesgue_integral_def max_def min_def intro!: set_lebesgue_integral_cong_AE)
lemma interval_integral_cong:
assumes "\<And>x. x \<in> einterval (min a b) (max a b) \<Longrightarrow> f x = g x"
shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g"
- using assms
-proof (induct a b rule: linorder_wlog)
- case (sym a b) then show ?case
- by (simp add: min.commute max.commute interval_integral_endpoints_reverse[of a b])
-next
- case (le a b) then show ?case
- by (auto simp: interval_lebesgue_integral_def max_def min_def
- intro!: set_lebesgue_integral_cong)
-qed
+ using assms by (simp add: interval_lebesgue_integral_def set_lebesgue_integral_cong)
lemma interval_lebesgue_integrable_cong_AE:
"f \<in> borel_measurable lborel \<Longrightarrow> g \<in> borel_measurable lborel \<Longrightarrow>
@@ -369,7 +351,7 @@
shows "f \<in> borel_measurable lborel \<Longrightarrow>
interval_lebesgue_integrable lborel a b (\<lambda>x. \<bar>f x\<bar>) = interval_lebesgue_integrable lborel a b f"
unfolding interval_lebesgue_integrable_def
- by (subst (1 2) set_integrable_abs_iff') simp_all
+ by (simp add: set_integrable_abs_iff')
lemma interval_integral_Icc:
fixes a b :: real
@@ -646,35 +628,29 @@
"incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
"l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b"
by (blast intro: einterval_Icc_approximation[OF \<open>a < b\<close>])
- have [simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
+ have aless[simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
by (rule order_less_le_trans, rule approx, force)
- have [simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
+ have lessb[simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
+ have cf: "\<And>i. continuous_on {min (l i) (u i)..max (l i) (u i)} f"
+ using approx f by (intro continuous_at_imp_continuous_on strip) auto
have FTCi: "\<And>i. (LBINT x=l i..u i. f x) = F (u i) - F (l i)"
- using assms approx apply (intro interval_integral_FTC_finite)
- apply (auto simp: less_imp_le min_def max_def
- has_real_derivative_iff_has_vector_derivative[symmetric])
- apply (rule continuous_at_imp_continuous_on, auto intro!: f)
- by (rule DERIV_subset [OF F], auto)
+ apply (intro interval_integral_FTC_finite cf DERIV_subset [OF F])
+ by (smt (verit) F aless approx(4) has_real_derivative_iff_has_vector_derivative has_vector_derivative_at_within lessb)
have 1: "\<And>i. set_integrable lborel {l i..u i} f"
- proof -
- fix i show "set_integrable lborel {l i .. u i} f"
- using \<open>a < l i\<close> \<open>u i < b\<close> unfolding set_integrable_def
- by (intro borel_integrable_compact f continuous_at_imp_continuous_on compact_Icc ballI)
- (auto simp flip: ereal_less_eq)
- qed
+ by (meson aless lessb assms(3) atLeastAtMost_iff borel_integrable_atLeastAtMost' continuous_at_imp_continuous_on)
have 2: "set_borel_measurable lborel (einterval a b) f"
unfolding set_borel_measurable_def
by (auto simp del: real_scaleR_def intro!: borel_measurable_continuous_on_indicator
simp: continuous_on_eq_continuous_at einterval_iff f)
- have 3: "(\<lambda>i. LBINT x=l i..u i. f x) \<longlonglongrightarrow> B - A"
- apply (subst FTCi)
- apply (intro tendsto_intros)
+ have "(\<lambda>x. F (l x)) \<longlonglongrightarrow> A"
+ using A approx unfolding tendsto_at_iff_sequentially comp_def
+ by (force elim!: allE[of _ "\<lambda>i. ereal (l i)"])
+ moreover have "(\<lambda>x. F (u x)) \<longlonglongrightarrow> B"
using B approx unfolding tendsto_at_iff_sequentially comp_def
- using tendsto_at_iff_sequentially[where 'a=real]
- apply (elim allE[of _ "\<lambda>i. ereal (u i)"], auto)
- using A approx unfolding tendsto_at_iff_sequentially comp_def
- by (elim allE[of _ "\<lambda>i. ereal (l i)"], auto)
+ by (force elim!: allE[of _ "\<lambda>i. ereal (u i)"])
+ ultimately have 3: "(\<lambda>i. LBINT x=l i..u i. f x) \<longlonglongrightarrow> B - A"
+ by (simp add: FTCi tendsto_diff)
show "(LBINT x=a..b. f x) = B - A"
by (rule interval_integral_Icc_approx_nonneg [OF \<open>a < b\<close> approx 1 f_nonneg 2 3])
show "set_integrable lborel (einterval a b) f"
@@ -820,11 +796,11 @@
by (metis antiderivative_continuous atLeastAtMost_iff image_subset_iff set_eq_subset)
have contfg: "continuous_on {a..b} (\<lambda>x. f (g x))"
by (blast intro: continuous_on_compose2 contf contg)
- have "LBINT x. indicat_real {a..b} x *\<^sub>R g' x *\<^sub>R f (g x) = F (g b) - F (g a)"
- apply (rule integral_FTC_atLeastAtMost
- [OF \<open>a \<le> b\<close> vector_diff_chain_within[OF v_derivg derivF, unfolded comp_def]])
- apply (auto intro!: continuous_on_scaleR contg' contfg)
- done
+ have "continuous_on {a..b} (\<lambda>x. g' x *\<^sub>R f (g x))"
+ by (auto intro!: continuous_on_scaleR contg' contfg)
+ then have "LBINT x. indicat_real {a..b} x *\<^sub>R g' x *\<^sub>R f (g x) = F (g b) - F (g a)"
+ using integral_FTC_atLeastAtMost [OF \<open>a \<le> b\<close> vector_diff_chain_within[OF v_derivg derivF]]
+ by force
then have "LBINT x=a..b. g' x *\<^sub>R f (g x) = F (g b) - F (g a)"
by (simp add: assms interval_integral_Icc set_lebesgue_integral_def)
moreover have "LBINT y=(g a)..(g b). f y = F (g b) - F (g a)"
@@ -924,12 +900,11 @@
apply (auto intro!: continuous_at_imp_continuous_on contf contg')
done
have "(\<lambda>i. LBINT x=l i..u i. g' x *\<^sub>R f (g x)) \<longlonglongrightarrow> (LBINT x=a..b. g' x *\<^sub>R f (g x))"
- apply (rule interval_integral_Icc_approx_integrable [OF \<open>a < b\<close> approx])
- by (rule assms)
+ using approx(4) \<open>a < b\<close> integrable interval_integral_Icc_approx_integrable by fastforce
hence 2: "(\<lambda>i. (LBINT y=g (l i)..g (u i). f y)) \<longlonglongrightarrow> (LBINT x=a..b. g' x *\<^sub>R f (g x))"
by (simp add: eq1)
have incseq: "incseq (\<lambda>i. {g (l i)<..<g (u i)})"
- apply (auto simp: incseq_def)
+ apply (clarsimp simp: incseq_def, intro conjI)
using lessb lle approx(5) g_nondec le_less_trans apply blast
by (force intro: less_le_trans)
have "(\<lambda>i. set_lebesgue_integral lborel {g (l i)<..<g (u i)} f)
@@ -988,13 +963,11 @@
have "A \<le> B" and un: "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
proof -
have A2: "(\<lambda>i. g (l i)) \<longlonglongrightarrow> A"
- using A apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
- by (drule_tac x = "\<lambda>i. ereal (l i)" in spec, auto)
+ using A by (force simp: einterval_def tendsto_at_iff_sequentially comp_def elim!: allE[where x = "\<lambda>i. ereal (l i)"])
hence A3: "\<And>i. g (l i) \<ge> A"
by (intro decseq_ge, auto simp: decseq_def)
have B2: "(\<lambda>i. g (u i)) \<longlonglongrightarrow> B"
- using B apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
- by (drule_tac x = "\<lambda>i. ereal (u i)" in spec, auto)
+ using B by (force simp: einterval_def tendsto_at_iff_sequentially comp_def elim!: allE[where x = "\<lambda>i. ereal (u i)"])
hence B3: "\<And>i. g (u i) \<le> B"
by (intro incseq_le, auto simp: incseq_def)
have "ereal (g (l 0)) \<le> ereal (g (u 0))"
@@ -1013,9 +986,7 @@
show "einterval A B \<subseteq> (\<Union>i. {g (l i)<..<g (u i)})"
by (auto simp: einterval_def AB)
show "(\<Union>i. {g (l i)<..<g (u i)}) \<subseteq> einterval A B"
- apply (clarsimp simp: einterval_def, intro conjI)
- using A3 le_ereal_less apply blast
- using B3 ereal_le_less by blast
+ using A3 B3 by (force simp: einterval_def intro: le_ereal_less ereal_le_less)
qed
qed
(* finally, the main argument *)
@@ -1030,7 +1001,7 @@
by (simp add: ac_simps)
qed
have incseq: "incseq (\<lambda>i. {g (l i)<..<g (u i)})"
- apply (clarsimp simp add: incseq_def, intro conjI)
+ apply (clarsimp simp: incseq_def, intro conjI)
apply (meson llb antimono_def approx(3) approx(5) g_nondec le_less_trans)
using alu uleu approx(6) g_nondec less_le_trans by blast
have img: "\<exists>c \<ge> l i. c \<le> u i \<and> x = g c" if "g (l i) \<le> x" "x \<le> g (u i)" for x i
@@ -1041,8 +1012,7 @@
using IVT' [of g] approx(4) dual_order.strict_implies_order by blast
qed
have "continuous_on {g (l i)..g (u i)} f" for i
- apply (intro continuous_intros continuous_at_imp_continuous_on)
- using contf img by force
+ using contf img by (force simp add: intro!: continuous_at_imp_continuous_on)
then have int_f: "\<And>i. set_integrable lborel {g (l i)<..<g (u i)} f"
by (rule set_integrable_subset [OF borel_integrable_atLeastAtMost']) (auto intro: less_imp_le)
have integrable: "set_integrable lborel (\<Union>i. {g (l i)<..<g (u i)}) f"
--- a/src/HOL/Analysis/Jordan_Curve.thy Fri Aug 04 19:17:49 2023 +0200
+++ b/src/HOL/Analysis/Jordan_Curve.thy Sun Aug 06 18:29:09 2023 +0100
@@ -42,9 +42,9 @@
(\<forall>x\<in>S \<union> T. (x - a) /\<^sub>R cmod (x - a) / ((x - b) /\<^sub>R cmod (x - b)) = exp (\<i>*complex_of_real (g x)))"
proof (cases "S \<inter> T = {}")
case True
- have "continuous_on (S \<union> T) (\<lambda>x. if x \<in> S then g x else h x)"
- apply (rule continuous_on_cases_local [OF clo contg conth])
- using True by auto
+ then have "continuous_on (S \<union> T) (\<lambda>x. if x \<in> S then g x else h x)"
+ using continuous_on_cases_local [OF clo contg conth]
+ by (meson disjoint_iff)
then show ?thesis
by (rule_tac x="(\<lambda>x. if x \<in> S then g x else h x)" in exI) (auto simp: g h)
next
@@ -54,11 +54,10 @@
have "exp (\<i>* of_real (g x)) = exp (\<i>* of_real (h x))"
using that by (simp add: g h)
then obtain n where "complex_of_real (g x) = complex_of_real (h x) + 2* of_int n*complex_of_real pi"
- apply (auto simp: exp_eq)
+ apply (simp add: exp_eq)
by (metis complex_i_not_zero distrib_left mult.commute mult_cancel_left)
then show ?thesis
- apply (rule_tac x=n in exI)
- using of_real_eq_iff by fastforce
+ using of_real_eq_iff by (fastforce intro!: exI [where x=n])
qed
have contgh: "continuous_on (S \<inter> T) (\<lambda>x. g x - h x)"
by (intro continuous_intros continuous_on_subset [OF contg] continuous_on_subset [OF conth]) auto
@@ -99,16 +98,16 @@
show ?thesis
proof (intro exI conjI)
show "continuous_on (S \<union> T) (\<lambda>x. if x \<in> S then g x else z + h x)"
- apply (intro continuous_intros continuous_on_cases_local [OF clo contg] conth)
- using z by fastforce
+ by (intro continuous_intros continuous_on_cases_local [OF clo contg] conth) (use z in force)
qed (auto simp: g h algebra_simps exp_add)
qed
- ultimately have *: "homotopic_with_canon (\<lambda>x. True) (S \<union> T) (sphere 0 1)
+ ultimately have "homotopic_with_canon (\<lambda>x. True) (S \<union> T) (sphere 0 1)
(\<lambda>x. (x - a) /\<^sub>R cmod (x - a)) (\<lambda>x. (x - b) /\<^sub>R cmod (x - b))"
by (subst homotopic_circlemaps_divide) (auto simp: inessential_eq_continuous_logarithm_circle)
- show ?thesis
- apply (rule Borsuk_maps_homotopic_in_connected_component_eq [THEN iffD1])
- using assms by (auto simp: *)
+ moreover have "compact (S \<union> T)"
+ using assms by blast
+ ultimately show ?thesis
+ using assms Borsuk_maps_homotopic_in_connected_component_eq by fastforce
qed
@@ -122,13 +121,8 @@
by (simp add: \<open>closed T\<close> ccT open_Compl open_path_connected_component)
then obtain g where g: "path g" "path_image g \<subseteq> - T" "pathstart g = a" "pathfinish g = b"
by (auto simp: path_component_def)
- obtain C where C: "compact C" "connected C" "a \<in> C" "b \<in> C" "C \<inter> T = {}"
- proof
- show "compact (path_image g)"
- by (simp add: \<open>path g\<close> compact_path_image)
- show "connected (path_image g)"
- by (simp add: \<open>path g\<close> connected_path_image)
- qed (use g in auto)
+ then obtain C where C: "compact C" "connected C" "a \<in> C" "b \<in> C" "C \<inter> T = {}"
+ by fastforce
obtain r where "0 < r" and r: "C \<union> S \<subseteq> ball 0 r"
by (metis \<open>compact C\<close> \<open>compact S\<close> bounded_Un compact_imp_bounded bounded_subset_ballD)
have "connected_component (- (S \<union> (T \<inter> cball 0 r \<union> sphere 0 r))) a b"
@@ -160,10 +154,9 @@
lemma Janiszewski_connected:
fixes S :: "complex set"
assumes ST: "compact S" "closed T" "connected(S \<inter> T)"
- and notST: "connected (- S)" "connected (- T)"
- shows "connected(- (S \<union> T))"
-using Janiszewski [OF ST]
-by (metis IntD1 IntD2 notST compl_sup connected_iff_connected_component)
+ and notST: "connected (- S)" "connected (- T)"
+ shows "connected(- (S \<union> T))"
+ using Janiszewski [OF ST] by (metis IntD1 IntD2 notST compl_sup connected_iff_connected_component)
subsection\<open>The Jordan Curve theorem\<close>
@@ -214,8 +207,8 @@
by (auto simp: path_image_subpath image_iff Bex_def)
qed
show "path_image (subpath 0 v h) \<union> path_image (subpath v 1 h) = path_image g"
- using v apply (simp add: path_image_subpath pihg [symmetric])
- using path_image_def by fastforce
+ using v path_image_subpath pihg path_image_def
+ by (metis (full_types) image_Un ivl_disj_un_two_touch(4))
qed
qed
@@ -257,7 +250,7 @@
by (meson \<open>simple_path c\<close> compact_imp_closed compact_simple_path_image outer open_Compl open_components)
show "connected outer"
using in_components_connected outer by blast
- show "inner \<inter> outer = {}"
+ show inner_outer: "inner \<inter> outer = {}"
by (meson \<open>\<not> bounded outer\<close> \<open>bounded inner\<close> \<open>connected outer\<close> bounded_subset components_maximal in_components_subset inner outer)
show fro_inner: "frontier inner = path_image c"
by (simp add: Jordan_Brouwer_frontier [OF hom inner])
@@ -267,14 +260,13 @@
proof -
have "frontier middle = path_image c"
by (simp add: Jordan_Brouwer_frontier [OF hom] that)
- have middle: "open middle" "connected middle" "middle \<noteq> {}"
- apply (meson \<open>simple_path c\<close> compact_imp_closed compact_simple_path_image m open_Compl open_components)
- using in_components_connected in_components_nonempty m by blast+
+ obtain middle: "open middle" "connected middle" "middle \<noteq> {}"
+ by (metis fro_inner frontier_closed in_components_maximal m open_Compl open_components)
obtain a0 b0 where "a0 \<in> path_image c" "b0 \<in> path_image c" "a0 \<noteq> b0"
using simple_path_image_uncountable [OF \<open>simple_path c\<close>]
by (metis Diff_cancel countable_Diff_eq countable_empty insert_iff subsetI subset_singleton_iff)
obtain a b g where ab: "a \<in> path_image c" "b \<in> path_image c" "a \<noteq> b"
- and "arc g" "pathstart g = a" "pathfinish g = b"
+ and g: "arc g" "pathstart g = a" "pathfinish g = b"
and pag_sub: "path_image g - {a,b} \<subseteq> middle"
proof (rule dense_accessible_frontier_point_pairs [OF \<open>open middle\<close> \<open>connected middle\<close>, of "path_image c \<inter> ball a0 (dist a0 b0)" "path_image c \<inter> ball b0 (dist a0 b0)"])
show "openin (top_of_set (frontier middle)) (path_image c \<inter> ball a0 (dist a0 b0))"
@@ -303,22 +295,21 @@
show "closed (path_image d \<union> path_image g)"
by (simp add: \<open>arc d\<close> \<open>arc g\<close> closed_Un closed_arc_image)
show "connected ((path_image u \<union> path_image g) \<inter> (path_image d \<union> path_image g))"
- by (metis Un_Diff_cancel \<open>arc g\<close> \<open>path_image u \<inter> path_image d = {a, b}\<close> \<open>pathfinish g = b\<close> \<open>pathstart g = a\<close> connected_arc_image insert_Diff1 pathfinish_in_path_image pathstart_in_path_image sup_bot.right_neutral sup_commute sup_inf_distrib1)
+ using ud_ab
+ by (metis Un_insert_left g connected_arc_image insert_absorb pathfinish_in_path_image pathstart_in_path_image sup_bot_left sup_commute sup_inf_distrib1)
show "connected_component (- (path_image u \<union> path_image g)) x y"
unfolding connected_component_def
proof (intro exI conjI)
have "connected ((inner \<union> (path_image c - path_image u)) \<union> (outer \<union> (path_image c - path_image u)))"
proof (rule connected_Un)
show "connected (inner \<union> (path_image c - path_image u))"
- apply (rule connected_intermediate_closure [OF \<open>connected inner\<close>])
- using fro_inner [symmetric] apply (auto simp: closure_subset frontier_def)
- done
+ using connected_intermediate_closure [OF \<open>connected inner\<close>]
+ by (metis Diff_subset closure_Un_frontier dual_order.refl fro_inner sup.mono sup_ge1)
show "connected (outer \<union> (path_image c - path_image u))"
- apply (rule connected_intermediate_closure [OF \<open>connected outer\<close>])
- using fro_outer [symmetric] apply (auto simp: closure_subset frontier_def)
- done
+ using connected_intermediate_closure [OF \<open>connected outer\<close>]
+ by (simp add: Diff_eq closure_Un_frontier fro_outer sup_inf_distrib1)
have "(inner \<inter> outer) \<union> (path_image c - path_image u) \<noteq> {}"
- by (metis \<open>arc d\<close> ud_ab Diff_Int Diff_cancel Un_Diff \<open>inner \<inter> outer = {}\<close> \<open>pathfinish d = a\<close> \<open>pathstart d = b\<close> arc_simple_path insert_commute nonempty_simple_path_endless sup_bot_left ud_Un)
+ using \<open>arc d\<close> \<open>pathfinish d = a\<close> \<open>pathstart d = b\<close> arc_imp_simple_path nonempty_simple_path_endless ud_Un ud_ab by fastforce
then show "(inner \<union> (path_image c - path_image u)) \<inter> (outer \<union> (path_image c - path_image u)) \<noteq> {}"
by auto
qed
@@ -344,13 +335,11 @@
have "connected ((inner \<union> (path_image c - path_image d)) \<union> (outer \<union> (path_image c - path_image d)))"
proof (rule connected_Un)
show "connected (inner \<union> (path_image c - path_image d))"
- apply (rule connected_intermediate_closure [OF \<open>connected inner\<close>])
- using fro_inner [symmetric] apply (auto simp: closure_subset frontier_def)
- done
+ using connected_intermediate_closure [OF \<open>connected inner\<close>] fro_inner
+ by (simp add: closure_Un_frontier sup.coboundedI2)
show "connected (outer \<union> (path_image c - path_image d))"
- apply (rule connected_intermediate_closure [OF \<open>connected outer\<close>])
- using fro_outer [symmetric] apply (auto simp: closure_subset frontier_def)
- done
+ using connected_intermediate_closure [OF \<open>connected outer\<close>]
+ by (simp add: closure_Un_frontier fro_outer sup.coboundedI2)
have "(inner \<inter> outer) \<union> (path_image c - path_image d) \<noteq> {}"
using \<open>arc u\<close> \<open>pathfinish u = b\<close> \<open>pathstart u = a\<close> arc_imp_simple_path nonempty_simple_path_endless ud_Un ud_ab by fastforce
then show "(inner \<union> (path_image c - path_image d)) \<inter> (outer \<union> (path_image c - path_image d)) \<noteq> {}"
@@ -393,8 +382,8 @@
corollary\<^marker>\<open>tag unimportant\<close> Jordan_disconnected:
fixes c :: "real \<Rightarrow> complex"
assumes "simple_path c" "pathfinish c = pathstart c"
- shows "\<not> connected(- path_image c)"
-using Jordan_curve [OF assms]
+ shows "\<not> connected(- path_image c)"
+ using Jordan_curve [OF assms]
by (metis Jordan_Brouwer_separation assms homeomorphic_simple_path_image_circle zero_less_one)
@@ -484,7 +473,7 @@
using Jordan_inside_outside [of "c1 +++ reversepath c"]
using Jordan_inside_outside [of "c2 +++ reversepath c"] assms
apply (simp_all add: path_image_join closed_Un closed_simple_path_image open_inside open_outside)
- apply (blast elim: | metis connected_simple_path_endless)+
+ apply (blast | metis connected_simple_path_endless)+
done
have inout_12: "inside (?\<Theta>1 \<union> ?\<Theta>2) \<inter> (?\<Theta> - {pathstart c, pathfinish c}) \<noteq> {}"
by (metis (no_types, lifting) c c1c ne_12 Diff_Int_distrib Diff_empty Int_empty_right Int_left_commute inf_sup_absorb inf_sup_aci(1) inside_no_overlap)
@@ -494,9 +483,8 @@
then show False
using connectedD [OF co_c, of "inside(?\<Theta>1 \<union> ?\<Theta>2)" "outside(?\<Theta>1 \<union> ?\<Theta>2)"]
using c c1c2 pa_c op_in12 op_out12 inout_12
- apply auto
- apply (metis Un_Diff_cancel2 Un_iff compl_sup disjoint_insert(1) inf_commute inf_compl_bot_left2 inside_Un_outside mk_disjoint_insert sup_inf_absorb)
- done
+ apply clarsimp
+ by (smt (verit, ccfv_threshold) Diff_Int_distrib Diff_cancel Diff_empty Int_assoc inf_sup_absorb inf_sup_aci(1) outside_no_overlap)
qed
have out_sub12: "outside(?\<Theta>1 \<union> ?\<Theta>2) \<subseteq> outside(?\<Theta>1 \<union> ?\<Theta>)" "outside(?\<Theta>1 \<union> ?\<Theta>2) \<subseteq> outside(?\<Theta>2 \<union> ?\<Theta>)"
by (metis Un_commute pi_disjoint outside_Un_outside_Un)+
@@ -507,10 +495,11 @@
by (metis (no_types) Diff_Int_distrib Diff_cancel inf_sup_absorb inf_sup_aci(3) inside_no_overlap)
have 2: "outside (?\<Theta> \<union> ?\<Theta>2) \<inter> ?\<Theta> = {}"
by (metis (no_types) Int_empty_right Int_left_commute inf_sup_absorb outside_no_overlap)
- have "outside (?\<Theta>2 \<union> ?\<Theta>) \<subseteq> outside (?\<Theta>1 \<union> ?\<Theta>2)"
- apply (subst Un_commute, rule outside_Un_outside_Un)
+ have "path_image c1 \<inter> outside (path_image c2 \<union> path_image c) = {}"
using connectedD [OF co_c1, of "inside(?\<Theta>2 \<union> ?\<Theta>)" "outside(?\<Theta>2 \<union> ?\<Theta>)"]
pa_c1 op_in2c op_out2c ne c1 c2c 1 2 by (auto simp: inf_sup_aci)
+ then have "outside (?\<Theta>2 \<union> ?\<Theta>) \<subseteq> outside (?\<Theta>1 \<union> ?\<Theta>2)"
+ by (metis outside_Un_outside_Un sup_commute)
with out_sub12
have "outside(?\<Theta>1 \<union> ?\<Theta>2) = outside(?\<Theta>2 \<union> ?\<Theta>)" by blast
then have "frontier(outside(?\<Theta>1 \<union> ?\<Theta>2)) = frontier(outside(?\<Theta>2 \<union> ?\<Theta>))"
@@ -548,9 +537,8 @@
then have xnot: "x \<notin> ?\<Theta>"
by (simp add: inside_def)
obtain z where zim: "z \<in> ?\<Theta>1" and zout: "z \<in> outside(?\<Theta>2 \<union> ?\<Theta>)"
- apply (auto simp: outside_inside)
- using nonempty_simple_path_endless [OF \<open>simple_path c1\<close>]
- by (metis Diff_Diff_Int Diff_iff ex_in_conv c1 c1c c1c2 pa1_disj_in2)
+ unfolding outside_inside
+ using nonempty_simple_path_endless [OF \<open>simple_path c1\<close>] c1 c1c c1c2 pa1_disj_in2 by auto
obtain e where "e > 0" and e: "ball z e \<subseteq> outside(?\<Theta>2 \<union> ?\<Theta>)"
using zout op_out2c open_contains_ball_eq by blast
have "z \<in> frontier (inside (?\<Theta>1 \<union> ?\<Theta>))"
@@ -560,11 +548,8 @@
then have w2: "w \<in> outside (?\<Theta>2 \<union> ?\<Theta>)"
by (metis e dist_commute mem_ball subsetCE)
then have "connected_component (- ?\<Theta>2 \<inter> - ?\<Theta>) z w"
- apply (simp add: connected_component_def)
- apply (rule_tac x = "outside(?\<Theta>2 \<union> ?\<Theta>)" in exI)
- using zout apply (auto simp: co_out2c)
- apply (simp_all add: outside_inside)
- done
+ unfolding connected_component_def
+ by (metis co_out2c compl_sup inside_Un_outside sup_ge2 zout)
moreover have "connected_component (- ?\<Theta>2 \<inter> - ?\<Theta>) w x"
unfolding connected_component_def
using pa2_disj_in1 co_in1c x w1 union_with_outside by fastforce
@@ -581,9 +566,8 @@
then have xnot: "x \<notin> ?\<Theta>"
by (simp add: inside_def)
obtain z where zim: "z \<in> ?\<Theta>2" and zout: "z \<in> outside(?\<Theta>1 \<union> ?\<Theta>)"
- apply (auto simp: outside_inside)
- using nonempty_simple_path_endless [OF \<open>simple_path c2\<close>]
- by (metis (no_types, opaque_lifting) Diff_Diff_Int Diff_iff c1c2 c2 c2c ex_in_conv pa2_disj_in1)
+ unfolding outside_inside
+ using nonempty_simple_path_endless [OF \<open>simple_path c2\<close>] c1c2 c2 c2c pa2_disj_in1 by auto
obtain e where "e > 0" and e: "ball z e \<subseteq> outside(?\<Theta>1 \<union> ?\<Theta>)"
using zout op_out1c open_contains_ball_eq by blast
have "z \<in> frontier (inside (?\<Theta>2 \<union> ?\<Theta>))"
@@ -593,11 +577,8 @@
then have w1: "w \<in> outside (?\<Theta>1 \<union> ?\<Theta>)"
by (metis e dist_commute mem_ball subsetCE)
then have "connected_component (- ?\<Theta>1 \<inter> - ?\<Theta>) z w"
- apply (simp add: connected_component_def)
- apply (rule_tac x = "outside(?\<Theta>1 \<union> ?\<Theta>)" in exI)
- using zout apply (auto simp: co_out1c)
- apply (simp_all add: outside_inside)
- done
+ unfolding connected_component_def
+ by (metis Compl_Un co_out1c inside_Un_outside sup_ge2 zout)
moreover have "connected_component (- ?\<Theta>1 \<inter> - ?\<Theta>) w x"
unfolding connected_component_def
using pa1_disj_in2 co_in2c x w2 union_with_outside by fastforce
@@ -614,8 +595,8 @@
have *: "outside (?\<Theta>1 \<union> ?\<Theta>) \<inter> outside (?\<Theta>2 \<union> ?\<Theta>) \<subseteq> outside (?\<Theta>1 \<union> ?\<Theta>2)"
proof (rule components_maximal)
show out_in: "outside (?\<Theta>1 \<union> ?\<Theta>2) \<in> components (- (?\<Theta>1 \<union> ?\<Theta>2))"
- apply (simp only: outside_in_components co_out12c)
- by (metis bounded_empty fr_out(1) frontier_empty unbounded_outside)
+ unfolding outside_in_components co_out12c
+ using co_out12c fr_out(1) by force
have conn_U: "connected (- (closure (inside (?\<Theta>1 \<union> ?\<Theta>)) \<union> closure (inside (?\<Theta>2 \<union> ?\<Theta>))))"
proof (rule Janiszewski_connected, simp_all)
show "bounded (inside (?\<Theta>1 \<union> ?\<Theta>))"
@@ -661,9 +642,10 @@
show "inside (?\<Theta>1 \<union> ?\<Theta>) \<union> inside (?\<Theta>2 \<union> ?\<Theta>) \<union> (?\<Theta> - {a, b}) = inside (?\<Theta>1 \<union> ?\<Theta>2)"
(is "?lhs = ?rhs")
proof
- show "?lhs \<subseteq> ?rhs"
- apply (simp add: in_sub_in1 in_sub_in2)
+ have " path_image c - {a, b} \<subseteq> inside (path_image c1 \<union> path_image c2)"
using c1c c2c inside_outside pi_disjoint by fastforce
+ then show "?lhs \<subseteq> ?rhs"
+ by (simp add: in_sub_in1 in_sub_in2)
have "inside (?\<Theta>1 \<union> ?\<Theta>2) \<subseteq> inside (?\<Theta>1 \<union> ?\<Theta>) \<union> inside (?\<Theta>2 \<union> ?\<Theta>) \<union> (?\<Theta>)"
using Compl_anti_mono [OF *] by (force simp: inside_outside)
moreover have "inside (?\<Theta>1 \<union> ?\<Theta>2) \<subseteq> -{a,b}"
--- a/src/HOL/Analysis/Locally.thy Fri Aug 04 19:17:49 2023 +0200
+++ b/src/HOL/Analysis/Locally.thy Sun Aug 06 18:29:09 2023 +0100
@@ -44,24 +44,18 @@
lemma open_neighbourhood_base_of:
"(\<forall>S. P S \<longrightarrow> openin X S)
\<Longrightarrow> neighbourhood_base_of P X \<longleftrightarrow> (\<forall>W x. openin X W \<and> x \<in> W \<longrightarrow> (\<exists>U. P U \<and> x \<in> U \<and> U \<subseteq> W))"
- apply (simp add: neighbourhood_base_of, safe, blast)
- by meson
+ by (smt (verit) neighbourhood_base_of subsetD)
lemma neighbourhood_base_of_open_subset:
"\<lbrakk>neighbourhood_base_of P X; openin X S\<rbrakk>
\<Longrightarrow> neighbourhood_base_of P (subtopology X S)"
- apply (clarsimp simp add: neighbourhood_base_of openin_subtopology_alt image_def)
- apply (rename_tac x V)
- apply (drule_tac x="S \<inter> V" in spec)
- apply (simp add: Int_ac)
- by (metis IntI le_infI1 openin_Int)
+ by (smt (verit, ccfv_SIG) neighbourhood_base_of openin_open_subtopology subset_trans)
lemma neighbourhood_base_of_topology_base:
"openin X = arbitrary union_of (\<lambda>W. W \<in> \<B>)
\<Longrightarrow> neighbourhood_base_of P X \<longleftrightarrow>
(\<forall>W x. W \<in> \<B> \<and> x \<in> W \<longrightarrow> (\<exists>U V. openin X U \<and> P V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> W))"
- apply (auto simp: openin_topology_base_unique neighbourhood_base_of)
- by (meson subset_trans)
+ by (smt (verit, del_insts) neighbourhood_base_of openin_topology_base_unique subset_trans)
lemma neighbourhood_base_at_unlocalized:
assumes "\<And>S T. \<lbrakk>P S; openin X T; x \<in> T; T \<subseteq> S\<rbrakk> \<Longrightarrow> P T"
@@ -86,9 +80,7 @@
lemma neighbourhood_base_at_with_subset:
"\<lbrakk>openin X U; x \<in> U\<rbrakk>
\<Longrightarrow> (neighbourhood_base_at x P X \<longleftrightarrow> neighbourhood_base_at x (\<lambda>T. T \<subseteq> U \<and> P T) X)"
- apply (simp add: neighbourhood_base_at_def)
- apply (metis IntI Int_subset_iff openin_Int)
- done
+ unfolding neighbourhood_base_at_def by (metis IntI Int_subset_iff openin_Int)
lemma neighbourhood_base_of_with_subset:
"neighbourhood_base_of P X \<longleftrightarrow> neighbourhood_base_of (\<lambda>t. t \<subseteq> topspace X \<and> P t) X"
@@ -140,9 +132,8 @@
qed
qed
moreover have ?Q if ?R
- using that
- apply (simp add: open_neighbourhood_base_of)
- by (metis mem_Collect_eq openin_subset path_component_of_refl path_connectedin_path_component_of path_connectedin_subtopology that topspace_subtopology_subset)
+ by (smt (verit) mem_Collect_eq open_neighbourhood_base_of openin_subset path_component_of_refl
+ path_connectedin_path_component_of path_connectedin_subtopology that topspace_subtopology_subset)
ultimately show "?P = ?Q" "?P = ?R"
by blast+
qed
@@ -154,23 +145,24 @@
lemma locally_path_connected_space_open_path_components:
"locally_path_connected_space X \<longleftrightarrow>
- (\<forall>U c. openin X U \<and> c \<in> path_components_of(subtopology X U) \<longrightarrow> openin X c)"
- apply (auto simp: locally_path_connected_space_eq_open_path_component_of path_components_of_def)
- by (metis imageI inf.absorb_iff2 openin_closedin_eq)
+ (\<forall>U C. openin X U \<and> C \<in> path_components_of(subtopology X U) \<longrightarrow> openin X C)"
+ apply (simp add: locally_path_connected_space_eq_open_path_component_of path_components_of_def)
+ by (smt (verit, ccfv_threshold) Int_iff image_iff openin_subset subset_iff)
lemma openin_path_component_of_locally_path_connected_space:
"locally_path_connected_space X \<Longrightarrow> openin X (Collect (path_component_of X x))"
- apply (auto simp: locally_path_connected_space_eq_open_path_component_of)
- by (metis openin_empty openin_topspace path_component_of_eq_empty subtopology_topspace)
+ using locally_path_connected_space_eq_open_path_component_of openin_subopen path_component_of_eq_empty
+ by fastforce
lemma openin_path_components_of_locally_path_connected_space:
- "\<lbrakk>locally_path_connected_space X; c \<in> path_components_of X\<rbrakk> \<Longrightarrow> openin X c"
- apply (auto simp: locally_path_connected_space_eq_open_path_component_of)
- by (metis (no_types, lifting) imageE openin_topspace path_components_of_def subtopology_topspace)
+ "\<lbrakk>locally_path_connected_space X; C \<in> path_components_of X\<rbrakk> \<Longrightarrow> openin X C"
+ using locally_path_connected_space_open_path_components by force
lemma closedin_path_components_of_locally_path_connected_space:
- "\<lbrakk>locally_path_connected_space X; c \<in> path_components_of X\<rbrakk> \<Longrightarrow> closedin X c"
- by (simp add: closedin_def complement_path_components_of_Union openin_path_components_of_locally_path_connected_space openin_clauses(3) path_components_of_subset)
+ "\<lbrakk>locally_path_connected_space X; C \<in> path_components_of X\<rbrakk> \<Longrightarrow> closedin X C"
+ unfolding closedin_def
+ by (metis Diff_iff complement_path_components_of_Union openin_clauses(3) openin_closedin_eq
+ openin_path_components_of_locally_path_connected_space)
lemma closedin_path_component_of_locally_path_connected_space:
assumes "locally_path_connected_space X"
@@ -193,8 +185,7 @@
(is "?lhs = ?rhs")
proof
assume ?lhs then show ?rhs
- apply (simp add: weakly_locally_path_connected_at_def neighbourhood_base_at_def)
- by (meson order_trans subsetD)
+ by (smt (verit) neighbourhood_base_at_def subset_iff weakly_locally_path_connected_at_def)
next
have *: "\<exists>V. path_connectedin X V \<and> U \<subseteq> V \<and> V \<subseteq> W"
if "(\<forall>y\<in>U. \<exists>C. path_connectedin X C \<and> C \<subseteq> W \<and> x \<in> C \<and> y \<in> C)"
@@ -218,18 +209,22 @@
(\<forall>V x. openin X V \<and> x \<in> V
\<longrightarrow> (\<exists>U. openin X U \<and>
x \<in> U \<and> U \<subseteq> V \<and>
- (\<forall>y \<in> U. \<exists>c. path_connectedin X c \<and>
- c \<subseteq> V \<and> x \<in> c \<and> y \<in> c)))"
- apply (simp add: locally_path_connected_space_def neighbourhood_base_of_def)
- apply (simp add: weakly_locally_path_connected_at flip: weakly_locally_path_connected_at_def)
- using openin_subset apply force
- done
+ (\<forall>y \<in> U. \<exists>C. path_connectedin X C \<and>
+ C \<subseteq> V \<and> x \<in> C \<and> y \<in> C)))"
+ (is "?lhs = ?rhs")
+proof
+ show "?lhs \<Longrightarrow> ?rhs"
+ by (metis locally_path_connected_space)
+ assume ?rhs
+ then show ?lhs
+ unfolding locally_path_connected_space_def neighbourhood_base_of
+ by (metis neighbourhood_base_at_def weakly_locally_path_connected_at weakly_locally_path_connected_at_def)
+qed
lemma locally_path_connected_space_open_subset:
- "\<lbrakk>locally_path_connected_space X; openin X s\<rbrakk>
- \<Longrightarrow> locally_path_connected_space (subtopology X s)"
- apply (simp add: locally_path_connected_space_def neighbourhood_base_of openin_open_subtopology path_connectedin_subtopology)
- by (meson order_trans)
+ "\<lbrakk>locally_path_connected_space X; openin X S\<rbrakk>
+ \<Longrightarrow> locally_path_connected_space (subtopology X S)"
+ by (smt (verit, best) locally_path_connected_space openin_open_subtopology path_connectedin_subtopology subset_trans)
lemma locally_path_connected_space_quotient_map_image:
assumes f: "quotient_map X Y f" and X: "locally_path_connected_space X"
@@ -247,19 +242,20 @@
let ?T = "Collect (path_component_of (subtopology X {z \<in> topspace X. f z \<in> V}) x)"
show "\<exists>T. openin X T \<and> x \<in> T \<and> T \<subseteq> {x \<in> topspace X. f x \<in> C}"
proof (intro exI conjI)
- have "\<exists>U. openin X U \<and> ?T \<in> path_components_of (subtopology X U)"
+ have *: "\<exists>U. openin X U \<and> ?T \<in> path_components_of (subtopology X U)"
proof (intro exI conjI)
show "openin X ({z \<in> topspace X. f z \<in> V})"
using V f openin_subset quotient_map_def by fastforce
- show "Collect (path_component_of (subtopology X {z \<in> topspace X. f z \<in> V}) x)
- \<in> path_components_of (subtopology X {z \<in> topspace X. f z \<in> V})"
- by (metis (no_types, lifting) Int_iff \<open>f x \<in> C\<close> c mem_Collect_eq path_component_in_path_components_of path_components_of_subset topspace_subtopology topspace_subtopology_subset x)
+ have "x \<in> topspace (subtopology X {z \<in> topspace X. f z \<in> V})"
+ using \<open>f x \<in> C\<close> c path_components_of_subset x by force
+ then show "Collect (path_component_of (subtopology X {z \<in> topspace X. f z \<in> V}) x)
+ \<in> path_components_of (subtopology X {z \<in> topspace X. f z \<in> V})"
+ by (meson path_component_in_path_components_of)
qed
with X show "openin X ?T"
using locally_path_connected_space_open_path_components by blast
show x: "x \<in> ?T"
- using V \<open>f x \<in> C\<close> c openin_subset path_component_of_equiv path_components_of_subset topspace_subtopology topspace_subtopology_subset x
- by fastforce
+ using * nonempty_path_components_of path_component_of_eq path_component_of_eq_empty by fastforce
have "f ` ?T \<subseteq> C"
proof (rule path_components_of_maximal)
show "C \<in> path_components_of (subtopology Y V)"
@@ -285,12 +281,9 @@
lemma homeomorphic_locally_path_connected_space:
assumes "X homeomorphic_space Y"
shows "locally_path_connected_space X \<longleftrightarrow> locally_path_connected_space Y"
-proof -
- obtain f g where "homeomorphic_maps X Y f g"
- using assms homeomorphic_space_def by fastforce
- then show ?thesis
- by (metis (no_types) homeomorphic_map_def homeomorphic_maps_map locally_path_connected_space_quotient_map_image)
-qed
+ using assms
+ unfolding homeomorphic_space_def homeomorphic_map_def homeomorphic_maps_map
+ by (metis locally_path_connected_space_quotient_map_image)
lemma locally_path_connected_space_retraction_map_image:
"\<lbrakk>retraction_map X Y r; locally_path_connected_space X\<rbrakk>
@@ -314,14 +307,21 @@
lemma path_component_eq_connected_component_of:
assumes "locally_path_connected_space X"
- shows "(path_component_of_set X x = connected_component_of_set X x)"
+ shows "path_component_of_set X x = connected_component_of_set X x"
proof (cases "x \<in> topspace X")
case True
- then show ?thesis
- using connectedin_connected_component_of [of X x]
- apply (clarsimp simp add: connectedin_def connected_space_clopen_in topspace_subtopology_subset cong: conj_cong)
- apply (drule_tac x="path_component_of_set X x" in spec)
- by (metis assms closedin_closed_subtopology closedin_connected_component_of closedin_path_component_of_locally_path_connected_space inf.absorb_iff2 inf.orderE openin_path_component_of_locally_path_connected_space openin_subtopology path_component_of_eq_empty path_component_subset_connected_component_of)
+ have "path_component_of_set X x \<subseteq> connected_component_of_set X x"
+ by (simp add: path_component_subset_connected_component_of)
+ moreover have "closedin X (path_component_of_set X x)"
+ by (simp add: assms closedin_path_component_of_locally_path_connected_space)
+ moreover have "openin X (path_component_of_set X x)"
+ by (simp add: assms openin_path_component_of_locally_path_connected_space)
+ moreover have "path_component_of_set X x \<noteq> {}"
+ by (meson True path_component_of_eq_empty)
+ ultimately show ?thesis
+ using connectedin_connected_component_of [of X x] unfolding connectedin_def
+ by (metis closedin_subset_topspace connected_space_clopen_in
+ subset_openin_subtopology topspace_subtopology_subset)
next
case False
then show ?thesis
@@ -356,8 +356,7 @@
obtain U C where U: "openin (product_topology X I) U"
and V: "path_connectedin (product_topology X I) C"
and "z \<in> U" "U \<subseteq> C" and Csub: "C \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
- using L apply (clarsimp simp add: locally_path_connected_space_def neighbourhood_base_of)
- by (metis openin_topspace topspace_product_topology z)
+ by (metis L locally_path_connected_space openin_topspace topspace_product_topology z)
then obtain V where finV: "finite {i \<in> I. V i \<noteq> topspace (X i)}"
and XV: "\<And>i. i\<in>I \<Longrightarrow> openin (X i) (V i)" and "z \<in> Pi\<^sub>E I V" and subU: "Pi\<^sub>E I V \<subseteq> U"
by (force simp: openin_product_topology_alt)
@@ -366,8 +365,7 @@
have "path_connected_space (X i)" if "i \<in> I" "V i = topspace (X i)" for i
proof -
have pc: "path_connectedin (X i) ((\<lambda>x. x i) ` C)"
- apply (rule path_connectedin_continuous_map_image [OF _ V])
- by (simp add: continuous_map_product_projection \<open>i \<in> I\<close>)
+ by (metis V continuous_map_product_projection path_connectedin_continuous_map_image that(1))
moreover have "((\<lambda>x. x i) ` C) = topspace (X i)"
proof
show "(\<lambda>x. x i) ` C \<subseteq> topspace (X i)"
@@ -388,8 +386,7 @@
using finite_subset by blast
next
show "locally_path_connected_space (X i)" if "i \<in> I" for i
- apply (rule locally_path_connected_space_quotient_map_image [OF _ L, where f = "\<lambda>x. x i"])
- by (metis False Abstract_Topology.retraction_imp_quotient_map retraction_map_product_projection that)
+ by (meson False L locally_path_connected_space_quotient_map_image quotient_map_product_projection that)
qed
qed
moreover have ?lhs if R: ?rhs
@@ -407,20 +404,12 @@
fix i assume "i \<in> I"
have "locally_path_connected_space (X i)"
by (simp add: R \<open>i \<in> I\<close>)
- moreover have "openin (X i) (W i) " "z i \<in> W i"
+ moreover have *:"openin (X i) (W i) " "z i \<in> W i"
using \<open>z \<in> Pi\<^sub>E I W\<close> opeW \<open>i \<in> I\<close> by auto
ultimately obtain U C where UC: "openin (X i) U" "path_connectedin (X i) C" "z i \<in> U" "U \<subseteq> C" "C \<subseteq> W i"
using \<open>i \<in> I\<close> by (force simp: locally_path_connected_space_def neighbourhood_base_of)
show "?\<Phi> i"
- proof (cases "W i = topspace (X i) \<and> path_connected_space(X i)")
- case True
- then show ?thesis
- using \<open>z i \<in> W i\<close> path_connectedin_topspace by blast
- next
- case False
- then show ?thesis
- by (meson UC)
- qed
+ by (metis UC * openin_subset path_connectedin_topspace)
qed
then obtain U C where
*: "\<And>i. i \<in> I \<Longrightarrow> openin (X i) (U i) \<and> path_connectedin (X i) (C i) \<and> z i \<in> (U i) \<and> (U i) \<subseteq> (C i) \<and> (C i) \<subseteq> W i \<and>
@@ -434,15 +423,12 @@
by (simp add: that finW)
ultimately have "finite {i \<in> I. U i \<noteq> topspace (X i)}"
using finite_subset by auto
- then have "openin (product_topology X I) (Pi\<^sub>E I U)"
- using * by (simp add: openin_PiE_gen)
+ with * have "openin (product_topology X I) (Pi\<^sub>E I U)"
+ by (simp add: openin_PiE_gen)
then show "\<exists>U. openin (product_topology X I) U \<and>
- (\<exists>V. path_connectedin (product_topology X I) V \<and> z \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> F)"
- apply (rule_tac x="PiE I U" in exI, simp)
- apply (rule_tac x="PiE I C" in exI)
- using \<open>z \<in> Pi\<^sub>E I W\<close> \<open>Pi\<^sub>E I W \<subseteq> F\<close> *
- apply (simp add: path_connectedin_PiE subset_PiE PiE_iff PiE_mono dual_order.trans)
- done
+ (\<exists>V. path_connectedin (product_topology X I) V \<and> z \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> F)"
+ by (metis (no_types, opaque_lifting) subsetI \<open>z \<in> Pi\<^sub>E I W\<close> \<open>Pi\<^sub>E I W \<subseteq> F\<close> * path_connectedin_PiE
+ PiE_iff PiE_mono order.trans)
qed
ultimately show ?thesis
using False by blast
@@ -507,7 +493,7 @@
show "\<exists>U V. openin (prod_topology X Y) U \<and> path_connectedin (prod_topology X Y) V \<and> (x, y) \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> UV"
apply (rule_tac x="C \<times> D" in exI)
apply (rule_tac x="K \<times> L" in exI)
- apply (auto simp: openin_prod_Times_iff path_connectedin_Times)
+ apply (fastforce simp: openin_prod_Times_iff path_connectedin_Times)
done
qed
qed
@@ -555,10 +541,10 @@
where "locally_connected_space X \<equiv> neighbourhood_base_of (connectedin X) X"
-lemma locally_connected_A: "(\<forall>U x. openin X U \<and> x \<in> U
- \<longrightarrow> openin X (connected_component_of_set (subtopology X U) x))
+lemma locally_connected_A: "(\<forall>U x. openin X U \<and> x \<in> U \<longrightarrow> openin X (connected_component_of_set (subtopology X U) x))
\<Longrightarrow> neighbourhood_base_of (\<lambda>U. openin X U \<and> connectedin X U) X"
- by (smt (verit, best) connected_component_of_refl connectedin_connected_component_of connectedin_subtopology mem_Collect_eq neighbourhood_base_of openin_subset topspace_subtopology_subset)
+ unfolding neighbourhood_base_of
+ by (metis (full_types) connected_component_of_refl connectedin_connected_component_of connectedin_subtopology mem_Collect_eq openin_subset topspace_subtopology_subset)
lemma locally_connected_B: "locally_connected_space X \<Longrightarrow>
(\<forall>U x. openin X U \<and> x \<in> U \<longrightarrow> openin X (connected_component_of_set (subtopology X U) x))"
@@ -594,12 +580,12 @@
lemma locally_connected_space_open_connected_components:
"locally_connected_space X \<longleftrightarrow>
(\<forall>U C. openin X U \<and> C \<in> connected_components_of(subtopology X U) \<longrightarrow> openin X C)"
- apply (simp add: locally_connected_space_eq_open_connected_component_of connected_components_of_def)
- by (smt (verit) imageE image_eqI inf.orderE inf_commute openin_subset)
+ unfolding connected_components_of_def locally_connected_space_eq_open_connected_component_of
+ by (smt (verit, best) image_iff openin_subset topspace_subtopology_subset)
lemma openin_connected_component_of_locally_connected_space:
"locally_connected_space X \<Longrightarrow> openin X (connected_component_of_set X x)"
- by (metis connected_component_of_eq_empty locally_connected_space_eq_open_connected_component_of openin_empty openin_topspace subtopology_topspace)
+ by (metis connected_component_of_eq_empty locally_connected_B openin_empty openin_topspace subtopology_topspace)
lemma openin_connected_components_of_locally_connected_space:
"\<lbrakk>locally_connected_space X; C \<in> connected_components_of X\<rbrakk> \<Longrightarrow> openin X C"
@@ -651,8 +637,8 @@
lemma locally_connected_space_open_subset:
"\<lbrakk>locally_connected_space X; openin X S\<rbrakk> \<Longrightarrow> locally_connected_space (subtopology X S)"
- apply (simp add: locally_connected_space_def)
- by (smt (verit, ccfv_threshold) connectedin_subtopology neighbourhood_base_of openin_open_subtopology subset_trans)
+ unfolding locally_connected_space_def neighbourhood_base_of
+ by (smt (verit) connectedin_subtopology 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"
@@ -731,9 +717,8 @@
by (simp add: locally_connected_at_def locally_path_connected_at_def neighbourhood_base_at_mono path_connectedin_imp_connectedin)
lemma weakly_locally_path_connected_imp_weakly_locally_connected_at:
- "weakly_locally_path_connected_at x X
- \<Longrightarrow> weakly_locally_connected_at x X"
- by (simp add: neighbourhood_base_at_mono path_connectedin_imp_connectedin weakly_locally_connected_at_def weakly_locally_path_connected_at_def)
+ "weakly_locally_path_connected_at x X \<Longrightarrow> weakly_locally_connected_at x X"
+ by (metis path_connectedin_imp_connectedin weakly_locally_connected_at weakly_locally_path_connected_at)
lemma interior_of_locally_connected_subspace_component:
@@ -859,8 +844,7 @@
have "connected_space (X i)" if "i \<in> I" "V i = topspace (X i)" for i
proof -
have pc: "connectedin (X i) ((\<lambda>x. x i) ` C)"
- apply (rule connectedin_continuous_map_image [OF _ V])
- by (simp add: continuous_map_product_projection \<open>i \<in> I\<close>)
+ by (metis V connectedin_continuous_map_image continuous_map_product_projection that(1))
moreover have "((\<lambda>x. x i) ` C) = topspace (X i)"
proof
show "(\<lambda>x. x i) ` C \<subseteq> topspace (X i)"
@@ -899,20 +883,12 @@
fix i assume "i \<in> I"
have "locally_connected_space (X i)"
by (simp add: R \<open>i \<in> I\<close>)
- moreover have "openin (X i) (W i) " "z i \<in> W i"
+ moreover have *: "openin (X i) (W i)" "z i \<in> W i"
using \<open>z \<in> Pi\<^sub>E I W\<close> opeW \<open>i \<in> I\<close> by auto
- ultimately obtain U C where UC: "openin (X i) U" "connectedin (X i) C" "z i \<in> U" "U \<subseteq> C" "C \<subseteq> W i"
+ ultimately obtain U C where "openin (X i) U" "connectedin (X i) C" "z i \<in> U" "U \<subseteq> C" "C \<subseteq> W i"
using \<open>i \<in> I\<close> by (force simp: locally_connected_space_def neighbourhood_base_of)
- show "?\<Phi> i"
- proof (cases "W i = topspace (X i) \<and> connected_space(X i)")
- case True
- then show ?thesis
- using \<open>z i \<in> W i\<close> connectedin_topspace by blast
- next
- case False
- then show ?thesis
- by (meson UC)
- qed
+ then show "?\<Phi> i"
+ by (metis * connectedin_topspace openin_subset)
qed
then obtain U C where
*: "\<And>i. i \<in> I \<Longrightarrow> openin (X i) (U i) \<and> connectedin (X i) (C i) \<and> z i \<in> (U i) \<and> (U i) \<subseteq> (C i) \<and> (C i) \<subseteq> W i \<and>
@@ -930,11 +906,8 @@
using * by (simp add: openin_PiE_gen)
then show "\<exists>U. openin (product_topology X I) U \<and>
(\<exists>V. connectedin (product_topology X I) V \<and> z \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> F)"
- apply (rule_tac x="PiE I U" in exI, simp)
- apply (rule_tac x="PiE I C" in exI)
using \<open>z \<in> Pi\<^sub>E I W\<close> \<open>Pi\<^sub>E I W \<subseteq> F\<close> *
- apply (simp add: connectedin_PiE subset_PiE PiE_iff PiE_mono dual_order.trans)
- done
+ by (metis (no_types, opaque_lifting) PiE_iff PiE_mono connectedin_PiE subset_iff)
qed
ultimately show ?thesis
using False by blast
@@ -990,27 +963,17 @@
shows "m \<le> n \<longrightarrow> X dim_le n"
using assms
proof (induction arbitrary: n rule: dimension_le.induct)
- case (1 m X)
- show ?case
- proof (intro strip dimension_le.intros)
- show "-1 \<le> n" if "m \<le> n" for n :: int using that using "1.hyps" by fastforce
- show "\<exists>U. a \<in> U \<and> U \<subseteq> V \<and> openin X U \<and> subtopology X (X frontier_of U) dim_le n-1"
- if "m \<le> n" and "openin X V" and "a \<in> V" for n V a
- using that by (meson "1.IH" diff_right_mono)
- qed
-qed
+qed (smt (verit) dimension_le.simps)
inductive_simps dim_le_minus2 [simp]: "X dim_le -2"
lemma dimension_le_eq_empty [simp]:
"X dim_le -1 \<longleftrightarrow> X = trivial_topology"
proof
- assume L: "X dim_le (-1)"
- show "X = trivial_topology"
- by (force intro: dimension_le.cases [OF L])
+ show "X dim_le (-1) \<Longrightarrow> X = trivial_topology"
+ by (force intro: dimension_le.cases)
next
- assume "X = trivial_topology"
- then show "X dim_le (-1)"
+ show "X = trivial_topology \<Longrightarrow> X dim_le (-1)"
using dimension_le.simps openin_subset by fastforce
qed
@@ -1144,7 +1107,8 @@
proof (cases "n \<ge> -1")
case True
then show ?thesis
- using homeomorphic_space_dimension_le_aux [of _ _ "nat(n+1)"] by (smt (verit) assms homeomorphic_space_sym nat_eq_iff)
+ using homeomorphic_space_dimension_le_aux [of _ _ "nat(n+1)"]
+ by (smt (verit) assms homeomorphic_space_sym nat_eq_iff)
next
case False
then show ?thesis