--- a/src/HOL/Finite_Set.thy Wed Aug 05 21:03:31 2020 +0100
+++ b/src/HOL/Finite_Set.thy Thu Aug 06 13:07:23 2020 +0100
@@ -1280,6 +1280,28 @@
lemma SUP_fold_sup: "finite A \<Longrightarrow> \<Squnion>(f ` A) = fold (sup \<circ> f) bot A"
using sup_SUP_fold_sup [of A bot] by simp
+lemma finite_Inf_in:
+ assumes "finite A" "A\<noteq>{}" and inf: "\<And>x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> inf x y \<in> A"
+ shows "Inf A \<in> A"
+proof -
+ have "Inf B \<in> A" if "B \<le> A" "B\<noteq>{}" for B
+ using finite_subset [OF \<open>B \<subseteq> A\<close> \<open>finite A\<close>] that
+ by (induction B) (use inf in \<open>force+\<close>)
+ then show ?thesis
+ by (simp add: assms)
+qed
+
+lemma finite_Sup_in:
+ assumes "finite A" "A\<noteq>{}" and sup: "\<And>x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> sup x y \<in> A"
+ shows "Sup A \<in> A"
+proof -
+ have "Sup B \<in> A" if "B \<le> A" "B\<noteq>{}" for B
+ using finite_subset [OF \<open>B \<subseteq> A\<close> \<open>finite A\<close>] that
+ by (induction B) (use sup in \<open>force+\<close>)
+ then show ?thesis
+ by (simp add: assms)
+qed
+
end
--- a/src/HOL/Fun_Def.thy Wed Aug 05 21:03:31 2020 +0100
+++ b/src/HOL/Fun_Def.thy Thu Aug 06 13:07:23 2020 +0100
@@ -217,6 +217,9 @@
and pair_lessI2: "a \<le> b \<Longrightarrow> s < t \<Longrightarrow> ((a, s), (b, t)) \<in> pair_less"
by (auto simp: pair_leq_def pair_less_def)
+lemma pair_less_iff1 [simp]: "((x,y), (x,z)) \<in> pair_less \<longleftrightarrow> y<z"
+ by (simp add: pair_less_def)
+
text \<open>Introduction rules for max\<close>
lemma smax_emptyI: "finite Y \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> ({}, Y) \<in> max_strict"
and smax_insertI:
--- a/src/HOL/Library/Infinite_Set.thy Wed Aug 05 21:03:31 2020 +0100
+++ b/src/HOL/Library/Infinite_Set.thy Thu Aug 06 13:07:23 2020 +0100
@@ -363,6 +363,13 @@
unfolding bij_betw_def by (auto intro: enumerate_in_set)
qed
+lemma
+ fixes S :: "nat set"
+ assumes S: "infinite S"
+ shows range_enumerate: "range (enumerate S) = S"
+ and strict_mono_enumerate: "strict_mono (enumerate S)"
+ by (auto simp add: bij_betw_imp_surj_on bij_enumerate assms strict_mono_def)
+
text \<open>A pair of weird and wonderful lemmas from HOL Light.\<close>
lemma finite_transitivity_chain:
assumes "finite A"