# HG changeset patch
# User paulson
# Date 1737154813 0
# Node ID e4ff4a4ee4ec277373255efa18f117afd424af7f
# Parent  a4c0f9d124403b1a0b51e2b4f6c7383a25c98900# Parent  1c003b308c98c35ba8b4b805b3a4972d2537988e
merged

diff -r a4c0f9d12440 -r e4ff4a4ee4ec src/HOL/Library/Ramsey.thy
--- a/src/HOL/Library/Ramsey.thy	Fri Jan 17 23:15:47 2025 +0100
+++ b/src/HOL/Library/Ramsey.thy	Fri Jan 17 23:00:13 2025 +0000
@@ -27,7 +27,7 @@
 lemma nsets_Pi_contra: "A' \<subseteq> A \<Longrightarrow> Pi ([A]\<^bsup>n\<^esup>) B \<subseteq> Pi ([A']\<^bsup>n\<^esup>) B"
   by (auto simp: nsets_def)
 
-lemma nsets_2_eq: "nsets A 2 = (\<Union>x\<in>A. \<Union>y\<in>A - {x}. {{x, y}})"
+lemma nsets_2_eq: "[A]\<^bsup>2\<^esup> = (\<Union>x\<in>A. \<Union>y\<in>A - {x}. {{x, y}})"
   by (auto simp: nsets_def card_2_iff)
 
 lemma nsets2_E:
@@ -41,7 +41,7 @@
 lemma doubleton_in_nsets_2 [simp]: "{x,y} \<in> [A]\<^bsup>2\<^esup> \<longleftrightarrow> x \<in> A \<and> y \<in> A \<and> x \<noteq> y"
   by (auto simp: nsets_2_eq Set.doubleton_eq_iff)
 
-lemma nsets_3_eq: "nsets A 3 = (\<Union>x\<in>A. \<Union>y\<in>A - {x}. \<Union>z\<in>A - {x,y}. {{x,y,z}})"
+lemma nsets_3_eq: "[A]\<^bsup>3\<^esup> = (\<Union>x\<in>A. \<Union>y\<in>A - {x}. \<Union>z\<in>A - {x,y}. {{x,y,z}})"
   by (simp add: eval_nat_numeral nsets_def card_Suc_eq) blast
 
 lemma nsets_4_eq: "[A]\<^bsup>4\<^esup> = (\<Union>u\<in>A. \<Union>x\<in>A - {u}. \<Union>y\<in>A - {u,x}. \<Union>z\<in>A - {u,x,y}. {{u,x,y,z}})"
@@ -49,9 +49,10 @@
 proof
   show "[A]\<^bsup>4\<^esup> \<subseteq> ?rhs"
     by (clarsimp simp add: nsets_def eval_nat_numeral card_Suc_eq) blast
-  show "?rhs \<subseteq> [A]\<^bsup>4\<^esup>"
-    apply (clarsimp simp add: nsets_def eval_nat_numeral card_Suc_eq)
-    by (metis insert_iff singletonD)
+  have "\<And>X. X \<in> ?rhs \<Longrightarrow> card X = 4"
+    by (force simp: card_2_iff)
+  then show "?rhs \<subseteq> [A]\<^bsup>4\<^esup>"
+    by (auto simp: nsets_def)
 qed
 
 lemma nsets_disjoint_2:
@@ -60,76 +61,75 @@
 
 lemma ordered_nsets_2_eq:
   fixes A :: "'a::linorder set"
-  shows "nsets A 2 = {{x,y} | x y. x \<in> A \<and> y \<in> A \<and> x<y}"
+  shows "[A]\<^bsup>2\<^esup> = {{x,y} | x y. x \<in> A \<and> y \<in> A \<and> x<y}"
      (is "_ = ?rhs")
 proof
-  show "nsets A 2 \<subseteq> ?rhs"
-    unfolding numeral_nat
-    apply (clarsimp simp add: nsets_def card_Suc_eq Set.doubleton_eq_iff not_less)
-    by (metis antisym)
-  show "?rhs \<subseteq> nsets A 2"
+  show "[A]\<^bsup>2\<^esup> \<subseteq> ?rhs"
+    by (auto simp: nsets_def card_2_iff doubleton_eq_iff neq_iff)
+  show "?rhs \<subseteq> [A]\<^bsup>2\<^esup>"
     unfolding numeral_nat by (auto simp: nsets_def card_Suc_eq)
 qed
 
 lemma ordered_nsets_3_eq:
   fixes A :: "'a::linorder set"
-  shows "nsets A 3 = {{x,y,z} | x y z. x \<in> A \<and> y \<in> A \<and> z \<in> A \<and> x<y \<and> y<z}"
+  shows "[A]\<^bsup>3\<^esup> = {{x,y,z} | x y z. x \<in> A \<and> y \<in> A \<and> z \<in> A \<and> x<y \<and> y<z}"
      (is "_ = ?rhs")
 proof
-  show "nsets A 3 \<subseteq> ?rhs"
-    apply (clarsimp simp add: nsets_def card_Suc_eq eval_nat_numeral)
-    by (metis insert_commute linorder_cases)
-  show "?rhs \<subseteq> nsets A 3"
-    apply (clarsimp simp add: nsets_def card_Suc_eq eval_nat_numeral)
-  by (metis empty_iff insert_iff not_less_iff_gr_or_eq)
+  show "[A]\<^bsup>3\<^esup> \<subseteq> ?rhs"
+    unfolding nsets_def card_3_iff
+    by (smt (verit, del_insts) Collect_mono_iff insert_commute insert_subset
+        linorder_less_linear)
+  have "\<And>X. X \<in> ?rhs \<Longrightarrow> card X = 3"
+    by (force simp: card_3_iff)
+  then show "?rhs \<subseteq> [A]\<^bsup>3\<^esup>"
+    by (auto simp: nsets_def)
 qed
 
 lemma ordered_nsets_4_eq:
   fixes A :: "'a::linorder set"
-  shows "[A]\<^bsup>4\<^esup> = {U. \<exists>u x y z. U = {u,x,y,z} \<and> u \<in> A \<and> x \<in> A \<and> y \<in> A \<and> z \<in> A \<and> u < x \<and> x < y \<and> y < z}"
-    (is "_ = Collect ?RHS")
+  defines "rhs \<equiv> \<lambda>U. \<exists>u x y z. U = {u,x,y,z} \<and> u \<in> A \<and> x \<in> A \<and> y \<in> A \<and> z \<in> A \<and> u < x \<and> x < y \<and> y < z"
+  shows "[A]\<^bsup>4\<^esup> = Collect rhs"
 proof -
-  have "?RHS U" if "U \<in> [A]\<^bsup>4\<^esup>" for U
+  have "rhs U" if "U \<in> [A]\<^bsup>4\<^esup>" for U
   proof -
     from that obtain l where "strict_sorted l" "List.set l = U" "length l = 4" "U \<subseteq> A"
       by (simp add: nsets_def) (metis finite_set_strict_sorted)
     then show ?thesis
-      unfolding numeral_nat length_Suc_conv by auto blast
+      unfolding numeral_nat length_Suc_conv rhs_def by auto blast
   qed
   moreover
-  have "Collect ?RHS \<subseteq> [A]\<^bsup>4\<^esup>"
-    apply (clarsimp simp add: nsets_def eval_nat_numeral)
-    apply (subst card_insert_disjoint, auto)+
-    done
+  have "\<And>X. X \<in> Collect rhs \<Longrightarrow> card X = 4 \<and> finite X \<and> X \<subseteq> A"
+    by (auto simp: rhs_def card_insert_if)
   ultimately show ?thesis
-    by auto
+    unfolding nsets_def by blast
 qed
 
 lemma ordered_nsets_5_eq:
   fixes A :: "'a::linorder set"
-  shows "[A]\<^bsup>5\<^esup> = {U. \<exists>u v x y z. U = {u,v,x,y,z} \<and> u \<in> A \<and> v \<in> A \<and> x \<in> A \<and> y \<in> A \<and> z \<in> A \<and> u < v \<and> v < x \<and> x < y \<and> y < z}"
-    (is "_ = Collect ?RHS")
+  defines "rhs \<equiv> \<lambda>U. \<exists>u v x y z. U = {u,v,x,y,z} \<and> u \<in> A \<and> v \<in> A \<and> x \<in> A \<and> y \<in> A \<and> z \<in> A \<and> u < v \<and> v < x \<and> x < y \<and> y < z"
+  shows "[A]\<^bsup>5\<^esup> = Collect rhs"
 proof -
-  have "?RHS U" if "U \<in> [A]\<^bsup>5\<^esup>" for U
+  have "rhs U" if "U \<in> [A]\<^bsup>5\<^esup>" for U
   proof -
     from that obtain l where "strict_sorted l" "List.set l = U" "length l = 5" "U \<subseteq> A"
-      apply (simp add: nsets_def)
-      by (metis finite_set_strict_sorted)
+      by (simp add: nsets_def) (metis finite_set_strict_sorted)
     then show ?thesis
-      unfolding numeral_nat length_Suc_conv by auto blast
+      unfolding numeral_nat length_Suc_conv rhs_def by auto blast
   qed
   moreover
-  have "Collect ?RHS \<subseteq> [A]\<^bsup>5\<^esup>"
-    apply (clarsimp simp add: nsets_def eval_nat_numeral)
-    apply (subst card_insert_disjoint, auto)+
-    done
+  have "\<And>X. X \<in> Collect rhs \<Longrightarrow> card X = 5 \<and> finite X \<and> X \<subseteq> A"
+    by (auto simp: rhs_def card_insert_if)
   ultimately show ?thesis
-    by auto
+    unfolding nsets_def by blast
 qed
 
 lemma binomial_eq_nsets: "n choose k = card (nsets {0..<n} k)"
-  apply (simp add: binomial_def nsets_def)
-  by (meson subset_eq_atLeast0_lessThan_finite)
+proof -
+  have "{K. K \<subseteq> {0..<n} \<and> card K = k} = {N. N \<subseteq> {0..<n} \<and> finite N \<and> card N = k}"
+    using infinite_super by blast
+  then show ?thesis
+    by (simp add: binomial_def nsets_def)
+qed
 
 lemma nsets_eq_empty_iff: "nsets A r = {} \<longleftrightarrow> finite A \<and> card A < r"
   unfolding nsets_def
@@ -157,9 +157,10 @@
   by (auto simp: nsets_def card_gt_0_iff subset_singleton_iff)
 
 lemma nsets_self [simp]: "nsets {..<m} m = {{..<m}}"
-  unfolding nsets_def
-  apply auto
-  by (metis add.left_neutral lessThan_atLeast0 lessThan_iff subset_card_intvl_is_intvl)
+proof
+  show "[{..<m}]\<^bsup>m\<^esup> \<subseteq> {{..<m}}"
+    by (force simp add: card_subset_eq nsets_def)
+qed (simp add: nsets_def)
 
 lemma nsets_zero [simp]: "nsets A 0 = {{}}"
   by (auto simp: nsets_def)
@@ -170,17 +171,16 @@
 lemma inj_on_nsets:
   assumes "inj_on f A"
   shows "inj_on (\<lambda>X. f ` X) ([A]\<^bsup>n\<^esup>)"
-  using assms unfolding nsets_def
-  by (metis (no_types, lifting) inj_on_inverseI inv_into_image_cancel mem_Collect_eq)
+  using assms by (simp add: nsets_def inj_on_def inj_on_image_eq_iff)
 
 lemma bij_betw_nsets:
   assumes "bij_betw f A B"
   shows "bij_betw (\<lambda>X. f ` X) ([A]\<^bsup>n\<^esup>) ([B]\<^bsup>n\<^esup>)"
 proof -
-  have "(`) f ` [A]\<^bsup>n\<^esup> = [f ` A]\<^bsup>n\<^esup>"
-    using assms
-    apply (auto simp: nsets_def bij_betw_def image_iff card_image inj_on_subset)
+  have "\<And>X. \<lbrakk>X \<subseteq> f ` A; finite X\<rbrakk> \<Longrightarrow> \<exists>Y\<subseteq>A. finite Y \<and> card Y = card X \<and> X = f ` Y"
     by (metis card_image inj_on_finite order_refl subset_image_inj)
+  then have "(`) f ` [A]\<^bsup>n\<^esup> = [f ` A]\<^bsup>n\<^esup>"
+    using assms by (auto simp: nsets_def bij_betw_def image_iff card_image inj_on_subset)
   with assms show ?thesis
     by (auto simp: bij_betw_def inj_on_nsets)
 qed
@@ -188,9 +188,14 @@
 lemma nset_image_obtains:
   assumes "X \<in> [f`A]\<^bsup>k\<^esup>" "inj_on f A"
   obtains Y where "Y \<in> [A]\<^bsup>k\<^esup>" "X = f ` Y"
-  using assms
-  apply (clarsimp simp add: nsets_def subset_image_iff)
-  by (metis card_image finite_imageD inj_on_subset)
+proof
+  show "X = f ` (A \<inter> f -` X)"
+    using assms by (auto simp: nsets_def)
+  then show "A Int (f -` X) \<in> [A]\<^bsup>k\<^esup>"
+    using assms
+    unfolding nsets_def mem_Collect_eq
+    by (metis card_image finite_image_iff inf_le1 subset_inj_on)
+qed
 
 lemma nsets_image_funcset:
   assumes "g \<in> S \<rightarrow> T" and "inj_on g S"
@@ -331,8 +336,12 @@
 qed
 
 lemma partn_lst_eq_partn: "partn_lst {..<n} [m,m] 2 = partn {..<n} m 2 {..<2::nat}"
-  apply (simp add: partn_lst_def partn_def numeral_2_eq_2)
-  by (metis less_2_cases numeral_2_eq_2 lessThan_iff nth_Cons_0 nth_Cons_Suc)
+proof -
+  have "\<And>i. i < 2 \<Longrightarrow> [m, m] ! i = m"
+    using less_2_cases_iff by force
+  then show ?thesis
+    by (auto simp: partn_lst_def partn_def numeral_2_eq_2 cong: conj_cong)
+qed
 
 lemma partn_lstE:
   assumes "partn_lst \<beta> \<alpha> \<gamma>" "f \<in> nsets \<beta> \<gamma>  \<rightarrow>  {..<l}" "length \<alpha> = l"
@@ -603,8 +612,7 @@
           using V by simp
         then have "u ` V \<in> nsets {..<p} (q2 - Suc 0)"
           using u_nsets [of _ "q2 - Suc 0"] nsets_mono [OF Vsub] Usub u
-          unfolding bij_betw_def nsets_def
-          by (fastforce elim!: subsetD)
+          unfolding bij_betw_def nsets_def by blast
         then have inq1: "?W \<in> nsets {..p} q2"
           unfolding nsets_def using \<open>q2 > 0\<close> card_insert_if by fastforce
         have invu_nsets: "inv_into {..<p2} u ` X \<in> nsets V r"
@@ -653,9 +661,9 @@
         then have "u ` V \<in> nsets {..p} q1"
           using V u_nsets by auto
         moreover have "f ` nsets (u ` V) (Suc r) \<subseteq> {j}"
-          using hj
+          using hj unfolding h_def image_subset_iff nsets_def
           apply (clarsimp simp add: h_def image_subset_iff nsets_def)
-          by (metis Zero_not_Suc card_eq_0_iff card_image subset_image_inj)
+          by (metis card_image finite_imageD subset_image_inj)
         ultimately show ?thesis
           using jzero not_less_eq by fastforce
       qed
@@ -792,7 +800,7 @@
               using Suc Suc.hyps(2) j by linarith
             have "nsets (u ` V) r \<subseteq> (\<lambda>x. (u ` x)) ` nsets V r"
               apply (clarsimp simp add: nsets_def image_iff)
-              by (metis card_eq_0_iff card_image image_is_empty subset_image_inj)
+              by (metis card_image finite_imageD subset_image_inj)
             then have "f ` nsets (u ` V) r \<subseteq> h ` nsets V r"
               by (auto simp: h_def)
             then show "f ` nsets (u ` V) r \<subseteq> {j}"
@@ -866,9 +874,8 @@
       show "card (v ` U) = m \<and> clique (v ` U) E \<or> card (v ` U) = n \<and> indep (v ` U) E"
         using i unfolding numeral_2_eq_2
           using gi U u
-          apply (simp add: image_subset_iff nsets_2_eq clique_def indep_def less_Suc_eq)
-          apply (auto simp: f_def nsets_def card_image inj_on_subset split: if_split_asm)
-          done
+          unfolding image_subset_iff nsets_2_eq clique_def indep_def less_Suc_eq
+          by (auto simp: f_def nsets_def card_image inj_on_subset split: if_splits)
     qed
   qed
   then show ?thesis
diff -r a4c0f9d12440 -r e4ff4a4ee4ec src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Fri Jan 17 23:15:47 2025 +0100
+++ b/src/HOL/Transcendental.thy	Fri Jan 17 23:00:13 2025 +0000
@@ -1985,6 +1985,9 @@
   finally show ?thesis .
 qed
 
+lemma exp_gt_self: "x < exp (x::real)"
+  using exp_gt_zero ln_less_self by fastforce
+
 lemma ln_one_plus_pos_lower_bound:
   fixes x :: real
   assumes a: "0 \<le> x" and b: "x \<le> 1"