# HG changeset patch # User paulson # 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 \ card s = 1 \ 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 \ 3" shows "coplanar s" proof - - have "card s \ 2 \ card s = Suc (Suc (Suc 0))" + consider "card s \ 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: \finite s\ 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: "(\B. B \ f ` A \ P B) \ (\B. B \ A \ 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\y" + using assms by (blast dest: card_eq_SucD) + lemma is_singleton_altdef: "is_singleton A \ 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 \ (\x. A = {x})" + by (simp add: card_Suc_eq) + lemma card_le_Suc0_iff_eq: assumes "finite A" shows "card A \ Suc 0 \ (\a1 \ A. \a2 \ 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 \ B \ F \ A \ B" by auto +lemma funcset_to_empty_iff: "A \ {} = (if A={} then UNIV else {})" + by auto + lemma Pi_eq_empty[simp]: "(\ x \ A. B x) = {} \ (\x\A. B x = {})" - apply (simp add: Pi_def) - apply auto - txt \Converse direction requires Axiom of Choice to exhibit a function - picking an element from each non-empty \<^term>\B x\\ - apply (drule_tac x = "\u. SOME y. y \ B u" in spec) - apply auto - apply (cut_tac P = "\y. y \ B x" in some_eq_ex) - apply auto - done +proof - + have "\x\A. B x = {}" if "\f. \y. y \ A \ f y \ B y" + using that [of "\u. SOME y. y \ 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 \ I \ f \ Pi I (B(i := A)) \ f \ Pi (I - {i}) B \ f i \ 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 \Composition With a Restricted Domain: \<^term>\compose\\ @@ -438,6 +435,9 @@ lemma PiE_iff: "f \ Pi\<^sub>E I X \ (\i\I. f i \ X i) \ f \ extensional I" by (simp add: PiE_def Pi_iff) +lemma ext_funcset_to_sing_iff [simp]: "A \\<^sub>E {a} = {\x\A. a}" + by (auto simp: PiE_def Pi_iff extensionalityI) + lemma PiE_restrict[simp]: "f \ Pi\<^sub>E A B \ 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 \ card A" + obtains B where "B \ A" "card B = k" +proof - + obtain h where h: "bij_betw h {0..finite A\ ex_bij_betw_nat_finite by blast + show thesis + proof + show "h ` {0.. A" + by (metis \k \ card A\ bij_betw_def h image_mono ivl_subset zero_le) + have "inj_on h {0..k \ card A\ bij_betw_def h inj_on_subset ivl_subset zero_le) + then show "card (h ` {0..Generic big monoid operation over intervals\