--- a/src/HOL/Library/Infinite_Set.thy Wed Apr 29 13:18:32 2020 +0200
+++ b/src/HOL/Library/Infinite_Set.thy Wed Apr 29 15:16:17 2020 +0100
@@ -244,15 +244,21 @@
declare enumerate_0 [simp del] enumerate_Suc [simp del]
lemma enumerate_step: "infinite S \<Longrightarrow> enumerate S n < enumerate S (Suc n)"
- apply (induct n arbitrary: S)
- apply (rule order_le_neq_trans)
- apply (simp add: enumerate_0 Least_le enumerate_in_set)
- apply (simp only: enumerate_Suc')
- apply (subgoal_tac "enumerate (S - {enumerate S 0}) 0 \<in> S - {enumerate S 0}")
- apply (blast intro: sym)
- apply (simp add: enumerate_in_set del: Diff_iff)
- apply (simp add: enumerate_Suc')
- done
+proof (induction n arbitrary: S)
+ case 0
+ then have "enumerate S 0 \<le> enumerate S (Suc 0)"
+ by (simp add: enumerate_0 Least_le enumerate_in_set)
+ moreover have "enumerate (S - {enumerate S 0}) 0 \<in> S - {enumerate S 0}"
+ by (meson "0.prems" enumerate_in_set infinite_remove)
+ 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')
+qed
lemma enumerate_mono: "m < n \<Longrightarrow> infinite S \<Longrightarrow> enumerate S m < enumerate S n"
by (induct m n rule: less_Suc_induct) (auto intro: enumerate_step)
@@ -330,18 +336,25 @@
qed
qed
+lemma inj_enumerate:
+ fixes S :: "'a::wellorder set"
+ assumes S: "infinite S"
+ shows "inj (enumerate S)"
+ unfolding inj_on_def
+proof clarsimp
+ show "\<And>x y. enumerate S x = enumerate S y \<Longrightarrow> x = y"
+ by (metis neq_iff enumerate_mono[OF _ \<open>infinite S\<close>])
+qed
+
+text \<open>To generalise this, we'd need a condition that all initial segments were finite\<close>
lemma bij_enumerate:
fixes S :: "nat set"
assumes S: "infinite S"
shows "bij_betw (enumerate S) UNIV S"
proof -
- have "\<And>n m. n \<noteq> m \<Longrightarrow> enumerate S n \<noteq> enumerate S m"
- using enumerate_mono[OF _ \<open>infinite S\<close>] by (auto simp: neq_iff)
- then have "inj (enumerate S)"
- by (auto simp: inj_on_def)
- moreover have "\<forall>s \<in> S. \<exists>i. enumerate S i = s"
+ have "\<forall>s \<in> S. \<exists>i. enumerate S i = s"
using enumerate_Ex[OF S] by auto
- moreover note \<open>infinite S\<close>
+ moreover note \<open>infinite S\<close> inj_enumerate
ultimately show ?thesis
unfolding bij_betw_def by (auto intro: enumerate_in_set)
qed
@@ -374,10 +387,13 @@
assume "S \<in> \<F>"
have "{T \<in> \<F>. S \<subseteq> T} = {}"
if "\<not> (\<exists>y. y \<in> {T \<in> \<F>. \<forall>U\<in>\<F>. \<not> T \<subset> U} \<and> S \<subseteq> y)"
- apply (rule finite_transitivity_chain [of _ "\<lambda>T U. S \<subseteq> T \<and> T \<subset> U"])
- apply (use assms that in auto)
- apply (blast intro: dual_order.trans psubset_imp_subset)
- done
+ proof -
+ have \<section>: "\<And>x. x \<in> \<F> \<and> S \<subseteq> x \<Longrightarrow> \<exists>y. y \<in> \<F> \<and> S \<subseteq> y \<and> x \<subset> y"
+ using that by (blast intro: dual_order.trans psubset_imp_subset)
+ show ?thesis
+ proof (rule finite_transitivity_chain [of _ "\<lambda>T U. S \<subseteq> T \<and> T \<subset> U"])
+ qed (use assms in \<open>auto intro: \<section>\<close>)
+ qed
with \<open>S \<in> \<F>\<close> show "\<exists>y. y \<in> {T \<in> \<F>. \<forall>U\<in>\<F>. \<not> T \<subset> U} \<and> S \<subseteq> y"
by blast
qed