# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1575905811 0
# Node ID d67924987c34b19f2f6d525fad31488d2efed572
# Parent  b1f3e86a4745d72b7a2f1ba0a6c16e84a51a4f5f
a few new and tidier proofs (mostly about finite sets)

diff -r b1f3e86a4745 -r d67924987c34 src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Mon Dec 09 11:17:34 2019 +0100
+++ b/src/HOL/Analysis/Starlike.thy	Mon Dec 09 15:36:51 2019 +0000
@@ -3580,23 +3580,26 @@
   have "card s = 0 \<or> card s = 1 \<or> card s = 2"
     using assms by linarith
   then show ?thesis using assms
-    using card_eq_SucD
-    by auto (metis collinear_2 numeral_2_eq_2)
+    using card_eq_SucD numeral_2_eq_2 by (force simp: card_1_singleton_iff)
 qed
 
 lemma coplanar_small:
   assumes "finite s" "card s \<le> 3"
     shows "coplanar s"
 proof -
-  have "card s \<le> 2 \<or> card s = Suc (Suc (Suc 0))"
+  consider "card s \<le> 2" | "card s = Suc (Suc (Suc 0))"
     using assms by linarith
-  then show ?thesis using assms
-    apply safe
-    apply (simp add: collinear_small collinear_imp_coplanar)
-    apply (safe dest!: card_eq_SucD)
-    apply (auto simp: coplanar_def)
-    apply (metis hull_subset insert_subset)
-    done
+  then show ?thesis
+  proof cases
+    case 1
+    then show ?thesis
+      by (simp add: \<open>finite s\<close> collinear_imp_coplanar collinear_small)
+  next
+    case 2
+    then show ?thesis
+      using hull_subset [of "{_,_,_}"]
+      by (fastforce simp: coplanar_def dest!: card_eq_SucD)
+  qed
 qed
 
 lemma coplanar_empty: "coplanar {}"
diff -r b1f3e86a4745 -r d67924987c34 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon Dec 09 11:17:34 2019 +0100
+++ b/src/HOL/Finite_Set.thy	Mon Dec 09 15:36:51 2019 +0000
@@ -319,7 +319,7 @@
 next
   case insert
   then show ?case
-    by (clarsimp simp del: image_insert simp add: image_insert [symmetric]) blast  
+    by (clarsimp simp del: image_insert simp add: image_insert [symmetric]) blast
 qed
 
 lemma all_subset_image: "(\<forall>B. B \<subseteq> f ` A \<longrightarrow> P B) \<longleftrightarrow> (\<forall>B. B \<subseteq> A \<longrightarrow> P(f ` B))"
@@ -1785,10 +1785,18 @@
   obtains x where "A = {x}"
   using assms by (auto simp: card_Suc_eq)
 
+lemma card_2_doubletonE:
+  assumes "card A = Suc (Suc 0)"
+  obtains x y where "A = {x,y}" "x\<noteq>y"
+  using assms by (blast dest: card_eq_SucD)
+
 lemma is_singleton_altdef: "is_singleton A \<longleftrightarrow> card A = 1"
   unfolding is_singleton_def
   by (auto elim!: card_1_singletonE is_singletonE simp del: One_nat_def)
 
+lemma card_1_singleton_iff: "card A = Suc 0 \<longleftrightarrow> (\<exists>x. A = {x})"
+  by (simp add: card_Suc_eq)
+
 lemma card_le_Suc0_iff_eq:
   assumes "finite A"
   shows "card A \<le> Suc 0 \<longleftrightarrow> (\<forall>a1 \<in> A. \<forall>a2 \<in> A. a1 = a2)" (is "?C = ?A")
diff -r b1f3e86a4745 -r d67924987c34 src/HOL/Library/Cardinality.thy
--- a/src/HOL/Library/Cardinality.thy	Mon Dec 09 11:17:34 2019 +0100
+++ b/src/HOL/Library/Cardinality.thy	Mon Dec 09 15:36:51 2019 +0000
@@ -161,7 +161,7 @@
 subclass finite
 proof
   from CARD_1 show "finite (UNIV :: 'a set)"
-    by (auto intro!: card_ge_0_finite)
+    using finite_UNIV_fun by fastforce
 qed
 
 end
diff -r b1f3e86a4745 -r d67924987c34 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Mon Dec 09 11:17:34 2019 +0100
+++ b/src/HOL/Library/FuncSet.thy	Mon Dec 09 15:36:51 2019 +0000
@@ -68,16 +68,16 @@
 lemma image_subset_iff_funcset: "F ` A \<subseteq> B \<longleftrightarrow> F \<in> A \<rightarrow> B"
   by auto
 
+lemma funcset_to_empty_iff: "A \<rightarrow> {} = (if A={} then UNIV else {})"
+  by auto
+
 lemma Pi_eq_empty[simp]: "(\<Pi> x \<in> A. B x) = {} \<longleftrightarrow> (\<exists>x\<in>A. B x = {})"
-  apply (simp add: Pi_def)
-  apply auto
-  txt \<open>Converse direction requires Axiom of Choice to exhibit a function
-  picking an element from each non-empty \<^term>\<open>B x\<close>\<close>
-  apply (drule_tac x = "\<lambda>u. SOME y. y \<in> B u" in spec)
-  apply auto
-  apply (cut_tac P = "\<lambda>y. y \<in> B x" in some_eq_ex)
-  apply auto
-  done
+proof -
+  have "\<exists>x\<in>A. B x = {}" if "\<And>f. \<exists>y. y \<in> A \<and> f y \<notin> B y" 
+    using that [of "\<lambda>u. SOME y. y \<in> B u"] some_in_eq by blast
+  then show ?thesis
+    by force
+qed
 
 lemma Pi_empty [simp]: "Pi {} B = UNIV"
   by (simp add: Pi_def)
@@ -149,11 +149,8 @@
 
 lemma Pi_fupd_iff: "i \<in> I \<Longrightarrow> f \<in> Pi I (B(i := A)) \<longleftrightarrow> f \<in> Pi (I - {i}) B \<and> f i \<in> A"
   apply auto
-  apply (drule_tac x=x in Pi_mem)
-  apply (simp_all split: if_split_asm)
-  apply (drule_tac x=i in Pi_mem)
-  apply (auto dest!: Pi_mem)
-  done
+  apply (metis PiE fun_upd_apply)
+  by force
 
 
 subsection \<open>Composition With a Restricted Domain: \<^term>\<open>compose\<close>\<close>
@@ -438,6 +435,9 @@
 lemma PiE_iff: "f \<in> Pi\<^sub>E I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i) \<and> f \<in> extensional I"
   by (simp add: PiE_def Pi_iff)
 
+lemma ext_funcset_to_sing_iff [simp]: "A \<rightarrow>\<^sub>E {a} = {\<lambda>x\<in>A. a}"
+  by (auto simp: PiE_def Pi_iff extensionalityI)
+
 lemma PiE_restrict[simp]:  "f \<in> Pi\<^sub>E A B \<Longrightarrow> restrict f A = f"
   by (simp add: extensional_restrict PiE_def)
 
diff -r b1f3e86a4745 -r d67924987c34 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Mon Dec 09 11:17:34 2019 +0100
+++ b/src/HOL/Set_Interval.thy	Mon Dec 09 15:36:51 2019 +0000
@@ -1644,6 +1644,22 @@
    apply (force intro: leI)+
   done
 
+lemma get_smaller_card:
+  assumes "finite A" "k \<le> card A"
+  obtains B where "B \<subseteq> A" "card B = k"
+proof -
+  obtain h where h: "bij_betw h {0..<card A} A"
+    using \<open>finite A\<close> ex_bij_betw_nat_finite by blast
+  show thesis
+  proof
+    show "h ` {0..<k} \<subseteq> A"
+      by (metis \<open>k \<le> card A\<close> bij_betw_def h image_mono ivl_subset zero_le)
+    have "inj_on h {0..<k}"
+      by (meson \<open>k \<le> card A\<close> bij_betw_def h inj_on_subset ivl_subset zero_le)
+    then show "card (h ` {0..<k}) = k"
+      by (simp add: card_image)
+  qed
+qed
 
 subsection \<open>Generic big monoid operation over intervals\<close>