author paulson Thu, 06 Aug 2020 13:07:23 +0100 changeset 72327 496cfe488d72 parent 72326 6b5421bd0fc3 child 72328 f978ecaf119a child 72330 8c547eac8381
a few more lemmas
 src/HOL/Finite_Set.thy file | annotate | diff | comparison | revisions src/HOL/Fun_Def.thy file | annotate | diff | comparison | revisions src/HOL/Library/Infinite_Set.thy file | annotate | diff | comparison | revisions
--- 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
+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
+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"
+
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"