# HG changeset patch # User wenzelm # Date 1631002623 -7200 # Node ID cbbd08df65bd55570519abc77e1aef6160673a01 # Parent 38c01d7e9f5bedcf80e022c3ea2b7ba293aad833# Parent 9d9e7ed01dbbffd8f13098df0c38245303dc379b merged diff -r 9d9e7ed01dbb -r cbbd08df65bd src/HOL/Analysis/Affine.thy --- a/src/HOL/Analysis/Affine.thy Mon Sep 06 14:05:22 2021 +0200 +++ b/src/HOL/Analysis/Affine.thy Tue Sep 07 10:17:03 2021 +0200 @@ -798,7 +798,7 @@ have "card {x - a |x. x \ s - {a}} = card (s - {a})" unfolding * by (simp add: card_image inj_on_def) also have "\ > DIM('a)" using assms(2) - unfolding card_Diff_singleton[OF assms(1) \a\s\] by auto + unfolding card_Diff_singleton[OF \a\s\] by auto finally show ?thesis apply (subst insert_Diff[OF \a\s\, symmetric]) apply (rule dependent_imp_affine_dependent) @@ -821,9 +821,7 @@ using \a\S\ by (auto simp: span_base span_diff intro: subset_le_dim) also have "\ < dim S + 1" by auto also have "\ \ card (S - {a})" - using assms - using card_Diff_singleton[OF assms(1) \a\S\] - by auto + using assms card_Diff_singleton[OF \a\S\] by auto finally show ?thesis apply (subst insert_Diff[OF \a\S\, symmetric]) apply (rule dependent_imp_affine_dependent) diff -r 9d9e7ed01dbb -r cbbd08df65bd src/HOL/Complex.thy --- a/src/HOL/Complex.thy Mon Sep 06 14:05:22 2021 +0200 +++ b/src/HOL/Complex.thy Tue Sep 07 10:17:03 2021 +0200 @@ -26,7 +26,6 @@ lemma complex_eq_iff: "x = y \ Re x = Re y \ Im x = Im y" by (auto intro: complex.expand) - subsection \Addition and Subtraction\ instantiation complex :: ab_group_add @@ -655,6 +654,9 @@ subsection \Basic Lemmas\ +lemma complex_of_real_code[code_unfold]: "of_real = (\x. Complex x 0)" + by (intro ext, auto simp: complex_eq_iff) + lemma complex_eq_0: "z=0 \ (Re z)\<^sup>2 + (Im z)\<^sup>2 = 0" by (metis zero_complex.sel complex_eqI sum_power2_eq_zero_iff) diff -r 9d9e7ed01dbb -r cbbd08df65bd src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Mon Sep 06 14:05:22 2021 +0200 +++ b/src/HOL/Finite_Set.thy Tue Sep 07 10:17:03 2021 +0200 @@ -1601,15 +1601,20 @@ using assms by (cases "finite y") (auto simp: card_insert_if) -lemma card_Diff_singleton: "finite A \ x \ A \ card (A - {x}) = card A - 1" - by (simp add: card_Suc_Diff1 [symmetric]) +lemma card_Diff_singleton: + assumes "x \ A" shows "card (A - {x}) = card A - 1" +proof (cases "finite A") + case True + with assms show ?thesis + by (simp add: card_Suc_Diff1 [symmetric]) +qed auto lemma card_Diff_singleton_if: - "finite A \ card (A - {x}) = (if x \ A then card A - 1 else card A)" + "card (A - {x}) = (if x \ A then card A - 1 else card A)" by (simp add: card_Diff_singleton) lemma card_Diff_insert[simp]: - assumes "finite A" and "a \ A" and "a \ B" + assumes "a \ A" and "a \ B" shows "card (A - insert a B) = card (A - B) - 1" proof - have "A - insert a B = (A - B) - {a}" @@ -1618,8 +1623,11 @@ using assms by (simp add: card_Diff_singleton) qed -lemma card_insert_le: "finite A \ card A \ card (insert x A)" - by (simp add: card_insert_if) +lemma card_insert_le: "card A \ card (insert x A)" +proof (cases "finite A") + case True + then show ?thesis by (simp add: card_insert_if) +qed auto lemma card_Collect_less_nat[simp]: "card {i::nat. i < n} = n" by (induct n) (simp_all add:less_Suc_eq Collect_disj_eq) @@ -1775,8 +1783,12 @@ by (blast intro: less_trans) qed -lemma card_Diff1_le: "finite A \ card (A - {x}) \ card A" - by (cases "x \ A") (simp_all add: card_Diff1_less less_imp_le) +lemma card_Diff1_le: "card (A - {x}) \ card A" +proof (cases "finite A") + case True + then show ?thesis + by (cases "x \ A") (simp_all add: card_Diff1_less less_imp_le) +qed auto lemma card_psubset: "finite B \ A \ B \ card A < card B \ A < B" by (erule psubsetI) blast @@ -1833,7 +1845,7 @@ lemma insert_partition: "x \ F \ \c1 \ insert x F. \c2 \ insert x F. c1 \ c2 \ c1 \ c2 = {} \ x \ \F = {}" - by auto (* somewhat slow *) + by auto lemma finite_psubset_induct [consumes 1, case_names psubset]: assumes finite: "finite A" diff -r 9d9e7ed01dbb -r cbbd08df65bd src/HOL/Library/Disjoint_Sets.thy --- a/src/HOL/Library/Disjoint_Sets.thy Mon Sep 06 14:05:22 2021 +0200 +++ b/src/HOL/Library/Disjoint_Sets.thy Tue Sep 07 10:17:03 2021 +0200 @@ -332,6 +332,12 @@ using f[THEN inj_onD] P[THEN partition_onD1] by (auto simp: disjnt_def) qed auto +lemma partition_on_insert: + assumes "disjnt p (\P)" + shows "partition_on A (insert p P) \ partition_on (A-p) P \ p \ A \ p \ {}" + using assms + by (auto simp: partition_on_def disjnt_iff pairwise_insert) + subsection \Finiteness of partitions\ lemma finitely_many_partition_on: diff -r 9d9e7ed01dbb -r cbbd08df65bd src/HOL/Quotient_Examples/Quotient_FSet.thy --- a/src/HOL/Quotient_Examples/Quotient_FSet.thy Mon Sep 06 14:05:22 2021 +0200 +++ b/src/HOL/Quotient_Examples/Quotient_FSet.thy Tue Sep 07 10:17:03 2021 +0200 @@ -819,8 +819,7 @@ lemma card_remove_fset_le1: shows "card_fset (remove_fset x xs) \ card_fset xs" - unfolding remove_fset card_fset - by (rule card_Diff1_le[OF finite_fset]) + by simp lemma card_psubset_fset: shows "ys |\| xs \ card_fset ys < card_fset xs \ ys |\| xs" @@ -835,21 +834,17 @@ lemma card_minus_insert_fset[simp]: assumes "a |\| A" and "a |\| B" shows "card_fset (A - insert_fset a B) = card_fset (A - B) - 1" - using assms - unfolding in_fset card_fset minus_fset - by (simp add: card_Diff_insert[OF finite_fset]) + using assms by (simp add: in_fset card_fset) lemma card_minus_subset_fset: assumes "B |\| A" shows "card_fset (A - B) = card_fset A - card_fset B" using assms - unfolding subset_fset card_fset minus_fset - by (rule card_Diff_subset[OF finite_fset]) + by (simp add: subset_fset card_fset card_Diff_subset) lemma card_minus_fset: shows "card_fset (A - B) = card_fset A - card_fset (A |\| B)" - unfolding inter_fset card_fset minus_fset - by (rule card_Diff_subset_Int) (simp) + by (simp add: card_fset card_Diff_subset_Int) subsection \concat_fset\