--- 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 {}"
--- 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")
--- 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
--- 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)
--- 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>