diff -r f424e164d752 -r 5e315defb038 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Sat May 09 17:20:04 2020 +0000
+++ b/src/HOL/Library/Infinite_Set.thy	Mon May 11 11:15:41 2020 +0100
@@ -399,4 +399,189 @@
   qed
 qed
 
+subsection \<open>Properties of @{term enumerate} on finite sets\<close>
+
+lemma finite_enumerate_in_set: "\<lbrakk>finite S; n < card S\<rbrakk> \<Longrightarrow> enumerate S n \<in> S"
+proof (induction n arbitrary: S)
+  case 0
+  then show ?case
+    by (metis all_not_in_conv card_empty enumerate.simps(1) not_less0 wellorder_Least_lemma(1))
+next
+  case (Suc n)
+  show ?case
+    using Suc.prems Suc.IH [of "S - {LEAST n. n \<in> S}"]
+    apply (simp add: enumerate.simps)
+    by (metis Diff_empty Diff_insert0 Suc_lessD card.remove less_Suc_eq)
+qed
+
+lemma finite_enumerate_step: "\<lbrakk>finite S; Suc n < card S\<rbrakk> \<Longrightarrow> enumerate S n < enumerate S (Suc n)"
+proof (induction n arbitrary: S)
+  case 0
+  then have "enumerate S 0 \<le> enumerate S (Suc 0)"
+    by (simp add: Least_le enumerate.simps(1) finite_enumerate_in_set)
+  moreover have "enumerate (S - {enumerate S 0}) 0 \<in> S - {enumerate S 0}"
+    by (metis 0 Suc_lessD Suc_less_eq card_Suc_Diff1 enumerate_in_set finite_enumerate_in_set)
+  then have "enumerate S 0 \<noteq> enumerate (S - {enumerate S 0}) 0"
+    by auto
+  ultimately show ?case
+    by (simp add: enumerate_Suc')
+next
+  case (Suc n)
+  then show ?case
+    by (simp add: enumerate_Suc' finite_enumerate_in_set)
+qed
+
+lemma finite_enumerate_mono: "\<lbrakk>m < n; finite S; n < card S\<rbrakk> \<Longrightarrow> enumerate S m < enumerate S n"
+  by (induct m n rule: less_Suc_induct) (auto intro: finite_enumerate_step)
+
+
+lemma finite_le_enumerate:
+  assumes "finite S" "n < card S"
+  shows "n \<le> enumerate S n"
+  using assms
+proof (induction n)
+  case 0
+  then show ?case by simp
+next
+  case (Suc n)
+  then have "n \<le> enumerate S n" by simp
+  also note finite_enumerate_mono[of n "Suc n", OF _ \<open>finite S\<close>]
+  finally show ?case
+    using Suc.prems(2) Suc_leI by blast
+qed
+
+lemma finite_enumerate:
+  assumes fS: "finite S"
+  shows "\<exists>r::nat\<Rightarrow>nat. strict_mono_on r {..<card S} \<and> (\<forall>n<card S. r n \<in> S)"
+  unfolding strict_mono_def
+  using finite_enumerate_in_set[OF fS] finite_enumerate_mono[of _ _ S] fS
+  by (metis lessThan_iff strict_mono_on_def)
+
+lemma finite_enumerate_Suc'':
+  fixes S :: "'a::wellorder set"
+  assumes "finite S" "Suc n < card S"
+  shows "enumerate S (Suc n) = (LEAST s. s \<in> S \<and> enumerate S n < s)"
+  using assms
+proof (induction n arbitrary: S)
+  case 0
+  then have "\<forall>s \<in> S. enumerate S 0 \<le> s"
+    by (auto simp: enumerate.simps intro: Least_le)
+  then show ?case
+    unfolding enumerate_Suc' enumerate_0[of "S - {enumerate S 0}"]
+    by (metis Diff_iff dual_order.strict_iff_order singletonD singletonI)
+next
+  case (Suc n S)
+  then have "Suc n < card (S - {enumerate S 0})"
+    using Suc.prems(2) finite_enumerate_in_set by force
+  then show ?case
+    apply (subst (1 2) enumerate_Suc')
+    apply (simp add: Suc)
+    apply (intro arg_cong[where f = Least] HOL.ext)
+    using finite_enumerate_mono[OF zero_less_Suc \<open>finite S\<close>, of n] Suc.prems
+    by (auto simp flip: enumerate_Suc')
+qed
+
+lemma finite_enumerate_initial_segment:
+  fixes S :: "'a::wellorder set"
+  assumes "finite S" "s \<in> S" and n: "n < card (S \<inter> {..<s})"
+  shows "enumerate (S \<inter> {..<s}) n = enumerate S n"
+  using n
+proof (induction n)
+  case 0
+  have "(LEAST n. n \<in> S \<and> n < s) = (LEAST n. n \<in> S)"
+  proof (rule Least_equality)
+    have "\<exists>t. t \<in> S \<and> t < s"
+      by (metis "0" card_gt_0_iff disjoint_iff_not_equal lessThan_iff)
+    then show "(LEAST n. n \<in> S) \<in> S \<and> (LEAST n. n \<in> S) < s"
+      by (meson LeastI Least_le le_less_trans)
+  qed (simp add: Least_le)
+  then show ?case
+    by (auto simp: enumerate_0)
+next
+  case (Suc n)
+  then have less_card: "Suc n < card S"
+    by (meson assms(1) card_mono inf_sup_ord(1) leD le_less_linear order.trans)
+  obtain t where t: "t \<in> {s \<in> S. enumerate S n < s}"
+    by (metis Infinite_Set.enumerate_step enumerate_in_set finite_enumerate_in_set finite_enumerate_step less_card mem_Collect_eq)
+  have "(LEAST x. x \<in> S \<and> x < s \<and> enumerate S n < x) = (LEAST s. s \<in> S \<and> enumerate S n < s)"
+       (is "_ = ?r")
+  proof (intro Least_equality conjI)
+    show "?r \<in> S"
+      by (metis (mono_tags, lifting) LeastI mem_Collect_eq t)
+    show "?r < s"
+      using not_less_Least [of _ "\<lambda>t. t \<in> S \<and> enumerate S n < t"] Suc assms 
+      by (metis (no_types, lifting) Int_Collect Suc_lessD finite_Int finite_enumerate_in_set finite_enumerate_step lessThan_def linorder_cases)
+    show "enumerate S n < ?r"
+      by (metis (no_types, lifting) LeastI mem_Collect_eq t)
+  qed (auto simp: Least_le)
+  then show ?case
+    using Suc assms by (simp add: finite_enumerate_Suc'' less_card)
+qed
+
+lemma finite_enumerate_Ex:
+  fixes S :: "'a::wellorder set"
+  assumes S: "finite S"
+    and s: "s \<in> S"
+  shows "\<exists>n<card S. enumerate S n = s"
+  using s S
+proof (induction s arbitrary: S rule: less_induct)
+  case (less s)
+  show ?case
+  proof (cases "\<exists>y\<in>S. y < s")
+    case True
+    let ?T = "S \<inter> {..<s}"
+    have "finite ?T"
+      using less.prems(2) by blast
+    have TS: "card ?T < card S"
+      using less.prems by (blast intro: psubset_card_mono [OF \<open>finite S\<close>])
+    from True have y: "\<And>x. Max ?T < x \<longleftrightarrow> (\<forall>s'\<in>S. s' < s \<longrightarrow> s' < x)"
+      by (subst Max_less_iff) (auto simp: \<open>finite ?T\<close>)
+    then have y_in: "Max ?T \<in> {s'\<in>S. s' < s}"
+      using Max_in \<open>finite ?T\<close> by fastforce
+    with less.IH[of "Max ?T" ?T] obtain n where n: "enumerate ?T n = Max ?T" "n < card ?T"
+      using \<open>finite ?T\<close> by blast
+    then have "Suc n < card S"
+      using TS less_trans_Suc by blast
+    with S n have "enumerate S (Suc n) = s"
+      by (subst finite_enumerate_Suc'') (auto simp: y finite_enumerate_initial_segment less finite_enumerate_Suc'' intro!: Least_equality)
+    then show ?thesis
+      using \<open>Suc n < card S\<close> by blast
+  next
+    case False
+    then have "\<forall>t\<in>S. s \<le> t" by auto
+    moreover have "0 < card S"
+      using card_0_eq less.prems by blast
+    ultimately show ?thesis
+      using \<open>s \<in> S\<close>
+      by (auto intro!: exI[of _ 0] Least_equality simp: enumerate_0)
+  qed
+qed
+
+lemma finite_bij_enumerate:
+  fixes S :: "'a::wellorder set"
+  assumes S: "finite S"
+  shows "bij_betw (enumerate S) {..<card S} S"
+proof -
+  have "\<And>n m. \<lbrakk>n \<noteq> m; n < card S; m < card S\<rbrakk> \<Longrightarrow> enumerate S n \<noteq> enumerate S m"
+    using finite_enumerate_mono[OF _ \<open>finite S\<close>] by (auto simp: neq_iff)
+  then have "inj_on (enumerate S) {..<card S}"
+    by (auto simp: inj_on_def)
+  moreover have "\<forall>s \<in> S. \<exists>i<card S. enumerate S i = s"
+    using finite_enumerate_Ex[OF S] by auto
+  moreover note \<open>finite S\<close>
+  ultimately show ?thesis
+    unfolding bij_betw_def by (auto intro: finite_enumerate_in_set)
+qed
+
+lemma ex_bij_betw_strict_mono_card:
+  fixes M :: "'a::wellorder set"
+  assumes "finite M" 
+  obtains h where "bij_betw h {..<card M} M" and "strict_mono_on h {..<card M}"
+proof
+  show "bij_betw (enumerate M) {..<card M} M"
+    by (simp add: assms finite_bij_enumerate)
+  show "strict_mono_on (enumerate M) {..<card M}"
+    by (simp add: assms finite_enumerate_mono strict_mono_on_def)
+qed
+
 end