# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1695491119 -3600
# Node ID 07c35dec9dacc6fb70bf7516c5799b425d38a59a
# Parent  f8595f6d39a59336ca4644c57b985f51f8ef0816
A few new or simplified proofs

diff -r f8595f6d39a5 -r 07c35dec9dac src/HOL/Analysis/Abstract_Topology_2.thy
--- a/src/HOL/Analysis/Abstract_Topology_2.thy	Sun Sep 17 18:56:35 2023 +0100
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy	Sat Sep 23 18:45:19 2023 +0100
@@ -16,8 +16,8 @@
 text \<open>Combination of Elementary and Abstract Topology\<close>
 
 lemma approachable_lt_le2: 
-    "(\<exists>(d::real) > 0. \<forall>x. Q x \<longrightarrow> f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> Q x \<longrightarrow> P x)"
-by (meson dense less_eq_real_def order_le_less_trans)
+  "(\<exists>(d::real) > 0. \<forall>x. Q x \<longrightarrow> f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> Q x \<longrightarrow> P x)"
+  by (meson dense less_eq_real_def order_le_less_trans)
 
 lemma triangle_lemma:
   fixes x y z :: real
@@ -113,7 +113,7 @@
 lemma connected_as_closed_union:
   assumes "connected C" "C = A \<union> B" "closed A" "closed B" "A \<noteq> {}" "B \<noteq> {}"
   shows "A \<inter> B \<noteq> {}"
-by (metis assms closed_Un connected_closed_set)
+  by (metis assms closed_Un connected_closed_set)
 
 lemma closedin_subset_trans:
   "closedin (top_of_set U) S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> T \<subseteq> U \<Longrightarrow>
@@ -126,13 +126,13 @@
   by (auto simp: openin_open)
 
 lemma closedin_compact:
-   "\<lbrakk>compact S; closedin (top_of_set S) T\<rbrakk> \<Longrightarrow> compact T"
-by (metis closedin_closed compact_Int_closed)
+  "\<lbrakk>compact S; closedin (top_of_set S) T\<rbrakk> \<Longrightarrow> compact T"
+  by (metis closedin_closed compact_Int_closed)
 
 lemma closedin_compact_eq:
   fixes S :: "'a::t2_space set"
   shows "compact S \<Longrightarrow> (closedin (top_of_set S) T \<longleftrightarrow> compact T \<and> T \<subseteq> S)"
-by (metis closedin_imp_subset closedin_compact closed_subset compact_imp_closed)
+  by (metis closedin_imp_subset closedin_compact closed_subset compact_imp_closed)
 
 
 subsection \<open>Closure\<close>
@@ -304,6 +304,11 @@
   then show ?thesis by auto
 qed
 
+lemma continuous_image_closure_subset:
+  assumes "continuous_on A f" "closure B \<subseteq> A"
+  shows   "f ` closure B \<subseteq> closure (f ` B)"
+  using assms by (meson closed_closure closure_subset continuous_on_subset image_closure_subset)
+
 subsection\<^marker>\<open>tag unimportant\<close> \<open>A function constant on a set\<close>
 
 definition constant_on  (infixl "(constant'_on)" 50)
diff -r f8595f6d39a5 -r 07c35dec9dac src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Sun Sep 17 18:56:35 2023 +0100
+++ b/src/HOL/Complex.thy	Sat Sep 23 18:45:19 2023 +0100
@@ -464,6 +464,10 @@
 lemmas Re_suminf = bounded_linear.suminf[OF bounded_linear_Re]
 lemmas Im_suminf = bounded_linear.suminf[OF bounded_linear_Im]
 
+lemma continuous_on_Complex [continuous_intros]:
+  "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. Complex (f x) (g x))"
+  unfolding Complex_eq by (intro continuous_intros)
+
 lemma tendsto_Complex [tendsto_intros]:
   "(f \<longlongrightarrow> a) F \<Longrightarrow> (g \<longlongrightarrow> b) F \<Longrightarrow> ((\<lambda>x. Complex (f x) (g x)) \<longlongrightarrow> Complex a b) F"
   unfolding Complex_eq by (auto intro!: tendsto_intros)
@@ -872,9 +876,6 @@
 lemma i_not_in_Reals [simp, intro]: "\<i> \<notin> \<real>"
   by (auto simp: complex_is_Real_iff)
 
-lemma powr_power_complex: "z \<noteq> 0 \<or> n \<noteq> 0 \<Longrightarrow> (z powr u :: complex) ^ n = z powr (of_nat n * u)"
-  by (induction n) (auto simp: algebra_simps powr_add)
-  
 lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re (cis a ^ n)"
   by (auto simp add: DeMoivre)
 
diff -r f8595f6d39a5 -r 07c35dec9dac src/HOL/Int.thy
--- a/src/HOL/Int.thy	Sun Sep 17 18:56:35 2023 +0100
+++ b/src/HOL/Int.thy	Sat Sep 23 18:45:19 2023 +0100
@@ -1487,6 +1487,9 @@
     using pos_zmult_eq_1_iff_lemma [OF L] L by force
 qed auto
 
+lemma zmult_eq_neg1_iff: "a * b = (-1 :: int) \<longleftrightarrow> a = 1 \<and> b = -1 \<or> a = -1 \<and> b = 1"
+  using zmult_eq_1_iff[of a "-b"] by auto
+
 lemma infinite_UNIV_int [simp]: "\<not> finite (UNIV::int set)"
 proof
   assume "finite (UNIV::int set)"
diff -r f8595f6d39a5 -r 07c35dec9dac src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Sun Sep 17 18:56:35 2023 +0100
+++ b/src/HOL/Topological_Spaces.thy	Sat Sep 23 18:45:19 2023 +0100
@@ -1076,38 +1076,12 @@
   unfolding Lim_def using tendsto_unique [of net f] by auto
 
 lemma Lim_ident_at: "\<not> trivial_limit (at x within s) \<Longrightarrow> Lim (at x within s) (\<lambda>x. x) = x"
-  by (rule tendsto_Lim[OF _ tendsto_ident_at]) auto
+  by (simp add: tendsto_Lim)
 
 lemma Lim_cong:
-  assumes "eventually (\<lambda>x. f x = g x) F" "F = G"
-  shows   "Lim F f = Lim G g"
-proof (cases "(\<exists>c. (f \<longlongrightarrow> c) F) \<and> F \<noteq> bot")
-  case True
-  then obtain c where c: "(f \<longlongrightarrow> c) F"
-    by blast
-  hence "Lim F f = c"
-    using True by (intro tendsto_Lim) auto
-  moreover have "(f \<longlongrightarrow> c) F \<longleftrightarrow> (g \<longlongrightarrow> c) G"
-    using assms by (intro filterlim_cong) auto
-  with True c assms have "Lim G g = c"
-    by (intro tendsto_Lim) auto
-  ultimately show ?thesis
-    by simp
-next
-  case False
-  show ?thesis
-  proof (cases "F = bot")
-    case True
-    thus ?thesis using assms
-      by (auto simp: Topological_Spaces.Lim_def)
-  next
-    case False
-    have "(f \<longlongrightarrow> c) F \<longleftrightarrow> (g \<longlongrightarrow> c) G" for c
-      using assms by (intro filterlim_cong) auto
-    thus ?thesis
-      by (auto simp: Topological_Spaces.Lim_def)
-  qed
-qed
+  assumes "\<forall>\<^sub>F x in F. f x = g x" "F = G"
+  shows "Lim F f = Lim F g"
+  unfolding t2_space_class.Lim_def using tendsto_cong assms by fastforce
 
 lemma eventually_Lim_ident_at:
   "(\<forall>\<^sub>F y in at x within X. P (Lim (at x within X) (\<lambda>x. x)) y) \<longleftrightarrow>
diff -r f8595f6d39a5 -r 07c35dec9dac src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sun Sep 17 18:56:35 2023 +0100
+++ b/src/HOL/Transcendental.thy	Sat Sep 23 18:45:19 2023 +0100
@@ -2480,6 +2480,11 @@
   for a b x :: real
   by (simp add: powr_def)
 
+lemma powr_power: 
+  fixes z:: "'a::{real_normed_field,ln}"
+  shows "z \<noteq> 0 \<or> n \<noteq> 0 \<Longrightarrow> (z powr u) ^ n = z powr (of_nat n * u)"
+  by (induction n) (auto simp: algebra_simps powr_add)
+
 lemma powr_powr_swap: "(x powr a) powr b = (x powr b) powr a"
   for a b x :: real
   by (simp add: powr_powr mult.commute)