# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1581937629 0
# Node ID 9edb7fb69bc259a25d9676ed5cbf62b7f5dcf08e
# Parent  d8fb621fea025baffe9a1a67f99e46287c4dae0e
a few new lemmas

diff -r d8fb621fea02 -r 9edb7fb69bc2 src/HOL/Library/Ramsey.thy
--- a/src/HOL/Library/Ramsey.thy	Tue Feb 11 12:55:35 2020 +0000
+++ b/src/HOL/Library/Ramsey.thy	Mon Feb 17 11:07:09 2020 +0000
@@ -22,6 +22,12 @@
   unfolding numeral_2_eq_2
   by (auto simp: nsets_def  elim!: card_2_doubletonE)
 
+lemma nsets_doubleton_2_eq [simp]: "[{x, y}]\<^bsup>2\<^esup> = (if x=y then {} else {{x, y}})"
+  by (auto simp: nsets_2_eq)
+
+lemma doubleton_in_nsets_2 [simp]: "{x,y} \<in> [A]\<^bsup>2\<^esup> \<longleftrightarrow> x \<in> A \<and> y \<in> A \<and> x \<noteq> y"
+  by (auto simp: nsets_2_eq Set.doubleton_eq_iff)
+
 lemma binomial_eq_nsets: "n choose k = card (nsets {0..<n} k)"
   apply (simp add: binomial_def nsets_def)
   by (meson subset_eq_atLeast0_lessThan_finite)
@@ -42,7 +48,7 @@
     using that card_mono leD by auto
 qed
 
-lemma nsets_eq_empty: "n < r \<Longrightarrow> nsets {..<n} r = {}"
+lemma nsets_eq_empty: "\<lbrakk>finite A; card A < r\<rbrakk> \<Longrightarrow> nsets A r = {}"
   by (simp add: nsets_eq_empty_iff)
 
 lemma nsets_empty_iff: "nsets {} r = (if r=0 then {{}} else {})"
@@ -80,6 +86,29 @@
     by (auto simp: bij_betw_def inj_on_nsets)
 qed
 
+lemma nset_image_obtains:
+  assumes "X \<in> [f`A]\<^bsup>k\<^esup>" "inj_on f A"
+  obtains Y where "Y \<in> [A]\<^bsup>k\<^esup>" "X = f ` Y"
+  using assms
+  apply (clarsimp simp add: nsets_def subset_image_iff)
+  by (metis card_image finite_imageD inj_on_subset)
+
+lemma nsets_image_funcset:
+  assumes "g \<in> S \<rightarrow> T" and "inj_on g S"
+  shows "(\<lambda>X. g ` X) \<in> [S]\<^bsup>k\<^esup> \<rightarrow> [T]\<^bsup>k\<^esup>"
+    using assms
+    by (fastforce simp add: nsets_def card_image inj_on_subset subset_iff simp flip: image_subset_iff_funcset)
+
+lemma nsets_compose_image_funcset:
+  assumes f: "f \<in> [T]\<^bsup>k\<^esup> \<rightarrow> D" and "g \<in> S \<rightarrow> T" and "inj_on g S"
+  shows "f \<circ> (\<lambda>X. g ` X) \<in> [S]\<^bsup>k\<^esup> \<rightarrow> D"
+proof -
+  have "(\<lambda>X. g ` X) \<in> [S]\<^bsup>k\<^esup> \<rightarrow> [T]\<^bsup>k\<^esup>"
+    using assms by (simp add: nsets_image_funcset)
+  then show ?thesis
+    using f by fastforce 
+qed
+
 subsubsection \<open>Partition predicates\<close>
 
 definition partn :: "'a set \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'b set \<Rightarrow> bool"
diff -r d8fb621fea02 -r 9edb7fb69bc2 src/HOL/Num.thy
--- a/src/HOL/Num.thy	Tue Feb 11 12:55:35 2020 +0000
+++ b/src/HOL/Num.thy	Mon Feb 17 11:07:09 2020 +0000
@@ -1107,8 +1107,11 @@
 lemma less_2_cases: "n < 2 \<Longrightarrow> n = 0 \<or> n = Suc 0"
   by (auto simp add: numeral_2_eq_2)
 
+lemma less_2_cases_iff: "n < 2 \<longleftrightarrow> n = 0 \<or> n = Suc 0"
+  by (auto simp add: numeral_2_eq_2)
+
 text \<open>Removal of Small Numerals: 0, 1 and (in additive positions) 2.\<close>
-text \<open>bh: Are these rules really a good idea?\<close>
+text \<open>bh: Are these rules really a good idea? LCP: well, it already happens for 0 and 1!\<close>
 
 lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)"
   by simp