# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1695657965 -3600
# Node ID 1b9388e6eb75e345fcab6eaee968f89f85f89c17
# Parent  e10ef4f9c84847ac381ee7fe6775257bbd27b69a
A few new theorems

diff -r e10ef4f9c848 -r 1b9388e6eb75 src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Sun Sep 24 15:55:42 2023 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy	Mon Sep 25 17:06:05 2023 +0100
@@ -447,6 +447,18 @@
     "simple_path c \<Longrightarrow> path_image c - {pathstart c,pathfinish c} \<noteq> {}"
   by (simp add: simple_path_endless)
 
+lemma simple_path_continuous_image:
+  assumes "simple_path f" "continuous_on (path_image f) g" "inj_on g (path_image f)"
+  shows   "simple_path (g \<circ> f)"
+  unfolding simple_path_def
+proof
+  show "path (g \<circ> f)"
+    using assms unfolding simple_path_def by (intro path_continuous_image) auto
+  from assms have [simp]: "g (f x) = g (f y) \<longleftrightarrow> f x = f y" if "x \<in> {0..1}" "y \<in> {0..1}" for x y
+    unfolding inj_on_def path_image_def using that by fastforce
+  show "loop_free (g \<circ> f)"
+    using assms(1) by (auto simp: loop_free_def simple_path_def)
+qed
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open>The operations on paths\<close>
 
diff -r e10ef4f9c848 -r 1b9388e6eb75 src/HOL/Analysis/Uniform_Limit.thy
--- a/src/HOL/Analysis/Uniform_Limit.thy	Sun Sep 24 15:55:42 2023 +0200
+++ b/src/HOL/Analysis/Uniform_Limit.thy	Mon Sep 25 17:06:05 2023 +0100
@@ -56,12 +56,28 @@
   unfolding uniform_limit_iff eventually_at
   by (fastforce dest: spec[where x = "e / 2" for e])
 
+lemma uniform_limit_compose:
+  assumes ul: "uniform_limit X g l F"  
+    and cont: "uniformly_continuous_on U f"
+    and g: "\<forall>\<^sub>F n in F. g n ` X \<subseteq> U" and l: "l ` X \<subseteq> U"
+  shows "uniform_limit X (\<lambda>a b. f (g a b)) (f \<circ> l) F"
+proof (rule uniform_limitI)
+  fix \<epsilon>::real
+  assume "0 < \<epsilon>" 
+  then obtain \<delta> where "\<delta> > 0" and \<delta>: "\<And>u v. \<lbrakk>u\<in>U; v\<in>U; dist u v < \<delta>\<rbrakk> \<Longrightarrow> dist (f u) (f v) < \<epsilon>"
+    by (metis cont uniformly_continuous_on_def)
+  show "\<forall>\<^sub>F n in F. \<forall>x\<in>X. dist (f (g n x)) ((f \<circ> l) x) < \<epsilon>"
+    using uniform_limitD [OF ul \<open>\<delta>>0\<close>] g unfolding o_def
+    by eventually_elim (use \<delta> l in blast)
+qed
+
 lemma metric_uniform_limit_imp_uniform_limit:
   assumes f: "uniform_limit S f a F"
   assumes le: "eventually (\<lambda>x. \<forall>y\<in>S. dist (g x y) (b y) \<le> dist (f x y) (a y)) F"
   shows "uniform_limit S g b F"
 proof (rule uniform_limitI)
-  fix e :: real assume "0 < e"
+  fix e :: real 
+  assume "0 < e"
   from uniform_limitD[OF f this] le
   show "\<forall>\<^sub>F x in F. \<forall>y\<in>S. dist (g x y) (b y) < e"
     by eventually_elim force
diff -r e10ef4f9c848 -r 1b9388e6eb75 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Sun Sep 24 15:55:42 2023 +0200
+++ b/src/HOL/Complex.thy	Mon Sep 25 17:06:05 2023 +0100
@@ -769,6 +769,14 @@
 lemma Im_sum[simp]: "Im (sum f s) = (\<Sum>x\<in>s. Im(f x))"
   by (induct s rule: infinite_finite_induct) auto
 
+lemma Rats_complex_of_real_iff [iff]: "complex_of_real x \<in> \<rat> \<longleftrightarrow> x \<in> \<rat>"
+proof -
+  have "\<And>a b. \<lbrakk>0 < b; x = complex_of_int a / complex_of_int b\<rbrakk> \<Longrightarrow> x \<in> \<rat>"
+    by (metis Rats_divide Rats_of_int Re_complex_of_real Re_divide_of_real of_real_of_int_eq)
+  then show ?thesis
+    by (auto simp: elim!: Rats_cases')
+qed
+
 lemma sum_Re_le_cmod: "(\<Sum>i\<in>I. Re (z i)) \<le> cmod (\<Sum>i\<in>I. z i)"
   by (metis Re_sum complex_Re_le_cmod)
 
diff -r e10ef4f9c848 -r 1b9388e6eb75 src/HOL/Complex_Analysis/Meromorphic.thy
--- a/src/HOL/Complex_Analysis/Meromorphic.thy	Sun Sep 24 15:55:42 2023 +0200
+++ b/src/HOL/Complex_Analysis/Meromorphic.thy	Mon Sep 25 17:06:05 2023 +0100
@@ -2,23 +2,6 @@
   imports Laurent_Convergence Riemann_Mapping
 begin
 
-lemma analytic_at_cong:
-  assumes "eventually (\<lambda>x. f x = g x) (nhds x)" "x = y"
-  shows "f analytic_on {x} \<longleftrightarrow> g analytic_on {y}"
-proof -
-  have "g analytic_on {x}" if "f analytic_on {x}" "eventually (\<lambda>x. f x = g x) (nhds x)" for f g
-  proof -
-    have "(\<lambda>y. f (x + y)) has_fps_expansion fps_expansion f x"
-      by (rule analytic_at_imp_has_fps_expansion) fact
-    also have "?this \<longleftrightarrow> (\<lambda>y. g (x + y)) has_fps_expansion fps_expansion f x"
-      using that by (intro has_fps_expansion_cong refl) (auto simp: nhds_to_0' eventually_filtermap)
-    finally show ?thesis
-      by (rule has_fps_expansion_imp_analytic)
-  qed
-  from this[of f g] this[of g f] show ?thesis using assms
-    by (auto simp: eq_commute)
-qed
-
 definition remove_sings :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> complex" where
   "remove_sings f z = (if \<exists>c. f \<midarrow>z\<rightarrow> c then Lim (at z) f else 0)"
 
@@ -2330,4 +2313,4 @@
   finally show ?thesis .
 qed
 
-end
\ No newline at end of file
+end
diff -r e10ef4f9c848 -r 1b9388e6eb75 src/HOL/Conditionally_Complete_Lattices.thy
--- a/src/HOL/Conditionally_Complete_Lattices.thy	Sun Sep 24 15:55:42 2023 +0200
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Mon Sep 25 17:06:05 2023 +0100
@@ -590,6 +590,68 @@
 lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditionally_complete_linorder, dense_linorder}} = y"
   by (auto intro!: cInf_eq_non_empty intro: dense_ge_bounded)
 
+lemma Sup_inverse_eq_inverse_Inf:
+  fixes f::"'b \<Rightarrow> 'a::{conditionally_complete_linorder,linordered_field}"
+  assumes "bdd_above (range f)" "L > 0" and geL: "\<And>x. f x \<ge> L"
+  shows "(SUP x. 1 / f x) = 1 / (INF x. f x)"
+proof (rule antisym)
+  have bdd_f: "bdd_below (range f)"
+    by (meson assms bdd_belowI2)
+  have "Inf (range f) \<ge> L"
+    by (simp add: cINF_greatest geL)
+  have bdd_invf: "bdd_above (range (\<lambda>x. 1 / f x))"
+  proof (rule bdd_aboveI2)
+    show "\<And>x. 1 / f x \<le> 1/L"
+      using assms by (auto simp: divide_simps)
+  qed
+  moreover have le_inverse_Inf: "1 / f x \<le> 1 / Inf (range f)" for x
+  proof -
+    have "Inf (range f) \<le> f x"
+      by (simp add: bdd_f cInf_lower)
+    then show ?thesis
+      using assms \<open>L \<le> Inf (range f)\<close> by (auto simp: divide_simps)
+  qed
+  ultimately show *: "(SUP x. 1 / f x) \<le> 1 / Inf (range f)"
+    by (auto simp: cSup_le_iff cINF_lower)
+  have "1 / (SUP x. 1 / f x) \<le> f y" for y
+  proof (cases "(SUP x. 1 / f x) < 0")
+    case True
+    with assms show ?thesis
+      by (meson less_asym' order_trans linorder_not_le zero_le_divide_1_iff)
+  next
+    case False
+    have "1 / f y \<le> (SUP x. 1 / f x)"
+      by (simp add: bdd_invf cSup_upper)
+    with False assms show ?thesis
+      by (metis (no_types) div_by_1 divide_divide_eq_right dual_order.strict_trans1 inverse_eq_divide 
+          inverse_le_imp_le mult.left_neutral)
+  qed
+  then have "1 / (SUP x. 1 / f x) \<le> Inf (range f)"
+    using bdd_f by (simp add: le_cInf_iff)
+  moreover have "(SUP x. 1 / f x) > 0"
+    using assms cSUP_upper [OF _ bdd_invf] by (meson UNIV_I less_le_trans zero_less_divide_1_iff)
+  ultimately show "1 / Inf (range f) \<le> (SUP t. 1 / f t)"
+    using \<open>L \<le> Inf (range f)\<close> \<open>L>0\<close> by (auto simp: field_simps)
+qed 
+
+lemma Inf_inverse_eq_inverse_Sup:
+  fixes f::"'b \<Rightarrow> 'a::{conditionally_complete_linorder,linordered_field}"
+  assumes "bdd_above (range f)" "L > 0" and geL: "\<And>x. f x \<ge> L"
+  shows  "(INF x. 1 / f x) = 1 / (SUP x. f x)"
+proof -
+  obtain M where "M>0" and M: "\<And>x. f x \<le> M"
+    by (meson assms cSup_upper dual_order.strict_trans1 rangeI)
+  have bdd: "bdd_above (range (inverse \<circ> f))"
+    using assms le_imp_inverse_le by (auto simp: bdd_above_def)
+  have "f x > 0" for x
+    using \<open>L>0\<close> geL order_less_le_trans by blast
+  then have [simp]: "1 / inverse(f x) = f x" "1 / M \<le> 1 / f x" for x
+    using M \<open>M>0\<close> by (auto simp: divide_simps)
+  show ?thesis
+    using Sup_inverse_eq_inverse_Inf [OF bdd, of "inverse M"] \<open>M>0\<close>
+    by (simp add: inverse_eq_divide)
+qed
+
 lemma Inf_insert_finite:
   fixes S :: "'a::conditionally_complete_linorder set"
   shows "finite S \<Longrightarrow> Inf (insert x S) = (if S = {} then x else min x (Inf S))"
diff -r e10ef4f9c848 -r 1b9388e6eb75 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Sun Sep 24 15:55:42 2023 +0200
+++ b/src/HOL/Int.thy	Mon Sep 25 17:06:05 2023 +0100
@@ -1738,6 +1738,12 @@
 lemma power_int_numeral [simp]: "power_int x (numeral n) = x ^ numeral n"
   by (simp add: power_int_def)
 
+lemma powi_numeral_reduce: "x powi numeral n = x * x powi int (pred_numeral n)"
+  by (simp add: numeral_eq_Suc)
+
+lemma powi_minus_numeral_reduce: "x powi - (numeral n) = inverse x * x powi - int(pred_numeral n)"
+  by (simp add: numeral_eq_Suc power_int_def)
+
 lemma int_cases4 [case_names nonneg neg]:
   fixes m :: int
   obtains n where "m = int n" | n where "n > 0" "m = -int n"