# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1596715643 -3600
# Node ID 496cfe488d721ca9c9a3acd5a53ff9746b38e0c8
# Parent  6b5421bd0fc365340f7e2b80c2b32255167a6e4c
a few more lemmas

diff -r 6b5421bd0fc3 -r 496cfe488d72 src/HOL/Finite_Set.thy
--- 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
 
 
diff -r 6b5421bd0fc3 -r 496cfe488d72 src/HOL/Fun_Def.thy
--- 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:
diff -r 6b5421bd0fc3 -r 496cfe488d72 src/HOL/Library/Infinite_Set.thy
--- 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"