# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1721746483 -3600
# Node ID e65eed943bee9057f88d021a7a30669293f007ad
# Parent  fbc859ccdaf34ba87df09cfae5c8173b3939de63
A lot of new material from the Ramsey development, including a couple of new simprules.

diff -r fbc859ccdaf3 -r e65eed943bee src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Mon Jul 22 22:55:19 2024 +0100
+++ b/src/HOL/Deriv.thy	Tue Jul 23 15:54:43 2024 +0100
@@ -1656,34 +1656,6 @@
     by (blast dest: DERIV_unique order_less_imp_le)
 qed
 
-lemma pos_deriv_imp_strict_mono:
-  assumes "\<And>x. (f has_real_derivative f' x) (at x)"
-  assumes "\<And>x. f' x > 0"
-  shows   "strict_mono f"
-proof (rule strict_monoI)
-  fix x y :: real assume xy: "x < y"
-  from assms and xy have "\<exists>z>x. z < y \<and> f y - f x = (y - x) * f' z"
-    by (intro MVT2) (auto dest: connectedD_interval)
-  then obtain z where z: "z > x" "z < y" "f y - f x = (y - x) * f' z" by blast
-  note \<open>f y - f x = (y - x) * f' z\<close>
-  also have "(y - x) * f' z > 0" using xy assms by (intro mult_pos_pos) auto
-  finally show "f x < f y" by simp
-qed
-
-proposition  deriv_nonneg_imp_mono:
-  assumes deriv: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
-  assumes nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
-  assumes ab: "a \<le> b"
-  shows "g a \<le> g b"
-proof (cases "a < b")
-  assume "a < b"
-  from deriv have "\<And>x. \<lbrakk>x \<ge> a; x \<le> b\<rbrakk> \<Longrightarrow> (g has_real_derivative g' x) (at x)" by simp
-  with MVT2[OF \<open>a < b\<close>] and deriv
-    obtain \<xi> where \<xi>_ab: "\<xi> > a" "\<xi> < b" and g_ab: "g b - g a = (b - a) * g' \<xi>" by blast
-  from \<xi>_ab ab nonneg have "(b - a) * g' \<xi> \<ge> 0" by simp
-  with g_ab show ?thesis by simp
-qed (insert ab, simp)
-
 
 subsubsection \<open>A function is constant if its derivative is 0 over an interval.\<close>
 
@@ -1927,6 +1899,74 @@
   apply (metis filterlim_at_top_mirror lim)
   done
 
+proposition deriv_nonpos_imp_antimono:
+  assumes deriv: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
+  assumes nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<le> 0"
+  assumes "a \<le> b"
+  shows "g b \<le> g a"
+proof -
+  have "- g a \<le> - g b" 
+  proof (intro DERIV_nonneg_imp_nondecreasing [where f = "\<lambda>x. - g x"] conjI exI)
+    fix x
+    assume x: "a \<le> x" "x \<le> b"
+    show "((\<lambda>x. - g x) has_real_derivative - g' x) (at x)"
+      by (simp add: DERIV_minus deriv x)
+    show "0 \<le> - g' x"
+      by (simp add: nonneg x)
+  qed (rule \<open>a\<le>b\<close>)
+  then show ?thesis by simp
+qed
+
+lemma DERIV_nonneg_imp_increasing_open:
+  fixes a b :: real
+    and f :: "real \<Rightarrow> real"
+  assumes "a \<le> b"
+    and "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> (\<exists>y. DERIV f x :> y \<and> y \<ge> 0)"
+    and con: "continuous_on {a..b} f"
+  shows "f a \<le> f b"
+proof (cases "a=b")
+  case False
+  with \<open>a\<le>b\<close> have "a<b" by simp
+  show ?thesis 
+  proof (rule ccontr)
+    assume f: "\<not> ?thesis"
+    have "\<exists>l z. a < z \<and> z < b \<and> DERIV f z :> l \<and> f b - f a = (b - a) * l"
+      by (rule MVT) (use assms \<open>a<b\<close> real_differentiable_def in \<open>force+\<close>)
+    then obtain l z where z: "a < z" "z < b" "DERIV f z :> l" and "f b - f a = (b - a) * l"
+      by auto
+    with assms z f show False
+      by (metis DERIV_unique diff_ge_0_iff_ge zero_le_mult_iff)
+  qed
+qed auto
+
+lemma DERIV_nonpos_imp_decreasing_open:
+  fixes a b :: real
+    and f :: "real \<Rightarrow> real"
+  assumes "a \<le> b"
+    and "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> \<exists>y. DERIV f x :> y \<and> y \<le> 0"
+    and con: "continuous_on {a..b} f"
+  shows "f a \<ge> f b"
+proof -
+  have "(\<lambda>x. -f x) a \<le> (\<lambda>x. -f x) b"
+  proof (rule DERIV_nonneg_imp_increasing_open [of a b])
+    show "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> \<exists>y. ((\<lambda>x. - f x) has_real_derivative y) (at x) \<and> 0 \<le> y"
+      using assms
+      by (metis Deriv.field_differentiable_minus neg_0_le_iff_le)
+    show "continuous_on {a..b} (\<lambda>x. - f x)"
+      using con continuous_on_minus by blast
+  qed (use assms in auto)
+  then show ?thesis
+    by simp
+qed
+
+
+proposition  deriv_nonneg_imp_mono: (*DELETE*)
+  assumes deriv: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
+  assumes nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
+  assumes ab: "a \<le> b"
+  shows "g a \<le> g b"
+  by (metis DERIV_nonneg_imp_nondecreasing atLeastAtMost_iff assms)
+
 text \<open>Derivative of inverse function\<close>
 
 lemma DERIV_inverse_function:
diff -r fbc859ccdaf3 -r e65eed943bee src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Mon Jul 22 22:55:19 2024 +0100
+++ b/src/HOL/Filter.thy	Tue Jul 23 15:54:43 2024 +0100
@@ -926,6 +926,10 @@
   "eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"
   by (rule eventually_at_top_linorder)
 
+lemma frequently_sequentially:
+  "frequently P sequentially \<longleftrightarrow> (\<forall>N. \<exists>n\<ge>N. P n)"
+  by (simp add: frequently_def eventually_sequentially)
+
 lemma sequentially_bot [simp, intro]: "sequentially \<noteq> bot"
   unfolding filter_eq_iff eventually_sequentially by auto
 
diff -r fbc859ccdaf3 -r e65eed943bee src/HOL/IMP/Compiler2.thy
--- a/src/HOL/IMP/Compiler2.thy	Mon Jul 22 22:55:19 2024 +0100
+++ b/src/HOL/IMP/Compiler2.thy	Tue Jul 23 15:54:43 2024 +0100
@@ -194,14 +194,15 @@
 lemma acomp_succs [simp]:
   "succs (acomp a) n = {n + 1 .. n + size (acomp a)}"
   by (induct a arbitrary: n) auto
-
-lemma acomp_size:
-  "(1::int) \<le> size (acomp a)"
-  by (induct a) auto
-
+ 
 lemma acomp_exits [simp]:
   "exits (acomp a) = {size (acomp a)}"
-  by (auto simp: exits_def acomp_size)
+proof -
+  have "Suc 0 \<le> length (acomp a)" 
+    by (induct a) auto
+  then show ?thesis
+    by (auto simp add: exits_def)
+qed
 
 lemma bcomp_succs:
   "0 \<le> i \<Longrightarrow>
diff -r fbc859ccdaf3 -r e65eed943bee src/HOL/Int.thy
--- a/src/HOL/Int.thy	Mon Jul 22 22:55:19 2024 +0100
+++ b/src/HOL/Int.thy	Tue Jul 23 15:54:43 2024 +0100
@@ -198,7 +198,7 @@
     then have \<open>int n \<ge> int 1\<close>
       by (rule of_nat_mono)
     with \<open>l - k = int n\<close> show ?Q
-      by simp
+      by (simp add: algebra_simps)
   qed
 qed
 
diff -r fbc859ccdaf3 -r e65eed943bee src/HOL/Num.thy
--- a/src/HOL/Num.thy	Mon Jul 22 22:55:19 2024 +0100
+++ b/src/HOL/Num.thy	Tue Jul 23 15:54:43 2024 +0100
@@ -677,6 +677,33 @@
 lemma not_numeral_less_zero: "\<not> numeral n < 0"
   by (simp add: not_less zero_le_numeral)
 
+lemma one_of_nat_le_iff [simp]: "1 \<le> of_nat k \<longleftrightarrow> 1 \<le> k"
+  using of_nat_le_iff [of 1] by simp
+
+lemma numeral_nat_le_iff [simp]: "numeral n \<le> of_nat k \<longleftrightarrow> numeral n \<le> k"
+  using of_nat_le_iff [of "numeral n"] by simp
+
+lemma of_nat_le_1_iff [simp]: "of_nat k \<le> 1 \<longleftrightarrow> k \<le> 1"
+  using of_nat_le_iff [of _ 1] by simp
+
+lemma of_nat_le_numeral_iff [simp]: "of_nat k \<le> numeral n \<longleftrightarrow> k \<le> numeral n"
+  using of_nat_le_iff [of _ "numeral n"] by simp
+
+lemma one_of_nat_less_iff [simp]: "1 < of_nat k \<longleftrightarrow> 1 < k"
+  using of_nat_less_iff [of 1] by simp
+
+lemma numeral_nat_less_iff [simp]: "numeral n < of_nat k \<longleftrightarrow> numeral n < k"
+  using of_nat_less_iff [of "numeral n"] by simp
+
+lemma of_nat_less_1_iff [simp]: "of_nat k < 1 \<longleftrightarrow> k < 1"
+  using of_nat_less_iff [of _ 1] by simp
+
+lemma of_nat_less_numeral_iff [simp]: "of_nat k < numeral n \<longleftrightarrow> k < numeral n"
+  using of_nat_less_iff [of _ "numeral n"] by simp
+
+lemma of_nat_eq_numeral_iff [simp]: "of_nat k = numeral n \<longleftrightarrow> k = numeral n"
+  using of_nat_eq_iff [of _ "numeral n"] by simp
+
 lemmas le_numeral_extra =
   zero_le_one not_one_le_zero
   order_refl [of 0] order_refl [of 1]
diff -r fbc859ccdaf3 -r e65eed943bee src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Mon Jul 22 22:55:19 2024 +0100
+++ b/src/HOL/Number_Theory/Residues.thy	Tue Jul 23 15:54:43 2024 +0100
@@ -283,8 +283,10 @@
   defines "R \<equiv> residue_ring (int p)"
 
 sublocale residues_prime < residues p
-  unfolding R_def residues_def
-  by (auto simp: p_prime prime_gt_1_int)
+proof
+  show "1 < int p"
+    using prime_gt_1_nat by auto
+qed
 
 context residues_prime
 begin
diff -r fbc859ccdaf3 -r e65eed943bee src/HOL/Real.thy
--- a/src/HOL/Real.thy	Mon Jul 22 22:55:19 2024 +0100
+++ b/src/HOL/Real.thy	Tue Jul 23 15:54:43 2024 +0100
@@ -750,16 +750,10 @@
 lemma less_RealD:
   assumes "cauchy Y"
   shows "x < Real Y \<Longrightarrow> \<exists>n. x < of_rat (Y n)"
-  apply (erule contrapos_pp)
-  apply (simp add: not_less)
-  apply (erule Real_leI [OF assms])
-  done
+  by (meson Real_leI assms leD leI)
 
 lemma of_nat_less_two_power [simp]: "of_nat n < (2::'a::linordered_idom) ^ n"
-  apply (induct n)
-   apply simp
-  apply (metis add_le_less_mono mult_2 of_nat_Suc one_le_numeral one_le_power power_Suc)
-  done
+  by auto
 
 lemma complete_real:
   fixes S :: "real set"
@@ -1620,6 +1614,18 @@
 lemma Rats_no_bot_less: "\<exists>q \<in> \<rat>. q < x" for x :: real
   by (auto intro!: bexI[of _ "of_int (\<lfloor>x\<rfloor> - 1)"]) linarith
 
+lemma floor_ceiling_diff_le: "0 \<le> r \<Longrightarrow> nat\<lfloor>real k - r\<rfloor> \<le> k - nat\<lceil>r\<rceil>"
+  by linarith
+
+lemma floor_ceiling_diff_le': "nat\<lfloor>r - real k\<rfloor> \<le> nat\<lceil>r\<rceil> - k"
+  by linarith
+
+lemma ceiling_floor_diff_ge: "nat\<lceil>r - real k\<rceil> \<ge> nat\<lfloor>r\<rfloor> - k"
+  by linarith
+
+lemma ceiling_floor_diff_ge': "r \<le> k \<Longrightarrow> nat\<lceil>r - real k\<rceil> \<le> k - nat\<lfloor>r\<rfloor>"
+  by linarith
+
 
 subsection \<open>Exponentiation with floor\<close>
 
diff -r fbc859ccdaf3 -r e65eed943bee src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Mon Jul 22 22:55:19 2024 +0100
+++ b/src/HOL/Set_Interval.thy	Tue Jul 23 15:54:43 2024 +0100
@@ -316,6 +316,71 @@
   with * show "a = b \<and> b = c" by auto
 qed simp
 
+text \<open>The following results generalise their namesakes in @{theory HOL.Nat} to intervals\<close>
+
+lemma lift_Suc_mono_le_ivl:
+  assumes mono: "\<And>n. n\<in>N \<Longrightarrow> f n \<le> f (Suc n)"
+    and "n \<le> n'" and subN: "{n..<n'} \<subseteq> N"
+  shows "f n \<le> f n'"
+proof (cases "n < n'")
+  case True
+  then show ?thesis
+    using subN
+  proof (induction n n' rule: less_Suc_induct)
+    case (1 i)
+    then show ?case
+      by (simp add: mono subsetD) 
+  next
+    case (2 i j k)
+    have "f i \<le> f j" "f j \<le> f k"
+      using 2 by force+
+    then show ?case by auto 
+  qed
+next
+  case False
+  with \<open>n \<le> n'\<close> show ?thesis by auto
+qed
+
+lemma lift_Suc_antimono_le_ivl:
+  assumes mono: "\<And>n. n\<in>N \<Longrightarrow> f n \<ge> f (Suc n)"
+    and "n \<le> n'" and subN: "{n..<n'} \<subseteq> N"
+  shows "f n \<ge> f n'"
+proof (cases "n < n'")
+  case True
+  then show ?thesis
+    using subN
+  proof (induction n n' rule: less_Suc_induct)
+    case (1 i)
+    then show ?case
+      by (simp add: mono subsetD) 
+  next
+    case (2 i j k)
+    have "f i \<ge> f j" "f j \<ge> f k"
+      using 2 by force+
+    then show ?case by auto 
+  qed
+next
+  case False
+  with \<open>n \<le> n'\<close> show ?thesis by auto
+qed
+
+lemma lift_Suc_mono_less_ivl:
+  assumes mono: "\<And>n. n\<in>N \<Longrightarrow> f n < f (Suc n)"
+    and "n < n'" and subN: "{n..<n'} \<subseteq> N"
+  shows "f n < f n'"
+  using \<open>n < n'\<close>
+  using subN
+proof (induction n n' rule: less_Suc_induct)
+  case (1 i)
+  then show ?case
+    by (simp add: mono subsetD) 
+next
+  case (2 i j k)
+  have "f i < f j" "f j < f k"
+    using 2 by force+
+  then show ?case by auto 
+qed
+
 end
 
 context no_top
@@ -2247,6 +2312,30 @@
   finally show ?thesis by metis
 qed
 
+lemma prod_divide_nat_ivl:
+  fixes f :: "nat \<Rightarrow> 'a::idom_divide"
+  shows "\<lbrakk> m \<le> n; n \<le> p; prod f {m..<n} \<noteq> 0\<rbrakk> \<Longrightarrow> prod f {m..<p} div prod f {m..<n} = prod f {n..<p}"
+  using prod.atLeastLessThan_concat [of m n p f,symmetric]
+  by (simp add: ac_simps)
+
+lemma prod_divide_split: (*FIXME: why is \<Prod> syntax not available?*)
+  fixes f:: "nat \<Rightarrow> 'a::idom_divide"
+  assumes "m \<le> n" "prod f {..<m} \<noteq> 0"
+  shows "(prod f {..n}) div (prod f {..<m}) = prod (\<lambda>i. f(n - i)) {..n - m}"
+proof -
+  have "\<And>i. i \<le> n-m \<Longrightarrow> \<exists>k\<ge>m. k \<le> n \<and> i = n-k"
+    by (metis Nat.le_diff_conv2 add.commute \<open>m\<le>n\<close> diff_diff_cancel diff_le_self order.trans)
+  then have eq: "{..n-m} = (-)n ` {m..n}"
+    by force
+  have inj: "inj_on ((-)n) {m..n}"
+    by (auto simp: inj_on_def)
+  have "prod (\<lambda>i. f(n - i)) {..n - m} = prod f {m..n}"
+    by (simp add: eq prod.reindex_cong [OF inj])
+  also have "\<dots> = prod f {..n} div prod f {..<m}"
+    using prod_divide_nat_ivl[of 0 "m" "Suc n" f] assms
+    by (force simp: atLeast0AtMost atLeast0LessThan atLeastLessThanSuc_atLeastAtMost)
+  finally show ?thesis by metis
+qed
 
 subsubsection \<open>Telescoping sums\<close>
 
diff -r fbc859ccdaf3 -r e65eed943bee src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Mon Jul 22 22:55:19 2024 +0100
+++ b/src/HOL/Topological_Spaces.thy	Tue Jul 23 15:54:43 2024 +0100
@@ -893,6 +893,15 @@
       simp: eventually_at_filter less_le
       elim: eventually_elim2)
 
+lemma (in order_topology)
+  shows at_within_Ici_at_right: "at a within {a..} = at_right a"
+    and at_within_Iic_at_left:  "at a within {..a} = at_left a"
+  using order_tendstoD(2)[OF tendsto_ident_at [where s = "{a<..}"]]
+  using order_tendstoD(1)[OF tendsto_ident_at[where s = "{..<a}"]]
+  by (auto intro!: order_class.order_antisym filter_leI
+      simp: eventually_at_filter less_le
+      elim: eventually_elim2)
+
 lemma (in order_topology) at_within_Icc_at: "a < x \<Longrightarrow> x < b \<Longrightarrow> at x within {a..b} = at x"
   by (rule at_within_open_subset[where S="{a<..<b}"]) auto
 
@@ -1237,7 +1246,7 @@
   by (simp add: strict_mono_def)
 
 lemma incseq_SucI: "(\<And>n. X n \<le> X (Suc n)) \<Longrightarrow> incseq X"
-  using lift_Suc_mono_le[of X] by (auto simp: incseq_def)
+  by (simp add: mono_iff_le_Suc)
 
 lemma incseqD: "incseq f \<Longrightarrow> i \<le> j \<Longrightarrow> f i \<le> f j"
   by (auto simp: incseq_def)
@@ -1252,7 +1261,7 @@
   unfolding incseq_def by auto
 
 lemma decseq_SucI: "(\<And>n. X (Suc n) \<le> X n) \<Longrightarrow> decseq X"
-  using order.lift_Suc_mono_le[OF dual_order, of X] by (auto simp: decseq_def)
+  by (simp add: antimono_iff_le_Suc)
 
 lemma decseqD: "decseq f \<Longrightarrow> i \<le> j \<Longrightarrow> f j \<le> f i"
   by (auto simp: decseq_def)
diff -r fbc859ccdaf3 -r e65eed943bee src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Mon Jul 22 22:55:19 2024 +0100
+++ b/src/HOL/Transcendental.thy	Tue Jul 23 15:54:43 2024 +0100
@@ -6988,7 +6988,7 @@
 end
   
 lemma sinh_real_strict_mono: "strict_mono (sinh :: real \<Rightarrow> real)"
-  by (rule pos_deriv_imp_strict_mono derivative_intros)+ auto
+  by (force intro: strict_monoI DERIV_pos_imp_increasing [where f=sinh] derivative_intros)
 
 lemma cosh_real_strict_mono:
   assumes "0 \<le> x" and "x < (y::real)"
@@ -7004,10 +7004,10 @@
 
 lemma tanh_real_strict_mono: "strict_mono (tanh :: real \<Rightarrow> real)"
 proof -
-  have *: "tanh x ^ 2 < 1" for x :: real
+  have "tanh x ^ 2 < 1" for x :: real
     using tanh_real_bounds[of x] by (simp add: abs_square_less_1 abs_if)
-  show ?thesis
-    by (rule pos_deriv_imp_strict_mono) (insert *, auto intro!: derivative_intros)
+  then show ?thesis
+    by (force intro!: strict_monoI DERIV_pos_imp_increasing [where f=tanh] derivative_intros)
 qed
 
 lemma sinh_real_abs [simp]: "sinh (abs x :: real) = abs (sinh x)"