--- a/src/HOL/Analysis/Affine.thy Fri Sep 03 19:56:03 2021 +0200
+++ b/src/HOL/Analysis/Affine.thy Fri Sep 03 22:53:11 2021 +0100
@@ -798,7 +798,7 @@
have "card {x - a |x. x \<in> s - {a}} = card (s - {a})"
unfolding * by (simp add: card_image inj_on_def)
also have "\<dots> > DIM('a)" using assms(2)
- unfolding card_Diff_singleton[OF assms(1) \<open>a\<in>s\<close>] by auto
+ unfolding card_Diff_singleton[OF \<open>a\<in>s\<close>] by auto
finally show ?thesis
apply (subst insert_Diff[OF \<open>a\<in>s\<close>, symmetric])
apply (rule dependent_imp_affine_dependent)
@@ -821,9 +821,7 @@
using \<open>a\<in>S\<close> by (auto simp: span_base span_diff intro: subset_le_dim)
also have "\<dots> < dim S + 1" by auto
also have "\<dots> \<le> card (S - {a})"
- using assms
- using card_Diff_singleton[OF assms(1) \<open>a\<in>S\<close>]
- by auto
+ using assms card_Diff_singleton[OF \<open>a\<in>S\<close>] by auto
finally show ?thesis
apply (subst insert_Diff[OF \<open>a\<in>S\<close>, symmetric])
apply (rule dependent_imp_affine_dependent)
--- a/src/HOL/Complex.thy Fri Sep 03 19:56:03 2021 +0200
+++ b/src/HOL/Complex.thy Fri Sep 03 22:53:11 2021 +0100
@@ -27,6 +27,7 @@
by (auto intro: complex.expand)
+
subsection \<open>Addition and Subtraction\<close>
instantiation complex :: ab_group_add
@@ -655,6 +656,9 @@
subsection \<open>Basic Lemmas\<close>
+lemma complex_of_real_code[code_unfold]: "of_real = (\<lambda>x. Complex x 0)"
+ by (intro ext, auto simp: complex_eq_iff)
+
lemma complex_eq_0: "z=0 \<longleftrightarrow> (Re z)\<^sup>2 + (Im z)\<^sup>2 = 0"
by (metis zero_complex.sel complex_eqI sum_power2_eq_zero_iff)
--- a/src/HOL/Finite_Set.thy Fri Sep 03 19:56:03 2021 +0200
+++ b/src/HOL/Finite_Set.thy Fri Sep 03 22:53:11 2021 +0100
@@ -1601,15 +1601,20 @@
using assms
by (cases "finite y") (auto simp: card_insert_if)
-lemma card_Diff_singleton: "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> card (A - {x}) = card A - 1"
- by (simp add: card_Suc_Diff1 [symmetric])
+lemma card_Diff_singleton:
+ assumes "x \<in> 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 \<Longrightarrow> card (A - {x}) = (if x \<in> A then card A - 1 else card A)"
+ "card (A - {x}) = (if x \<in> A then card A - 1 else card A)"
by (simp add: card_Diff_singleton)
lemma card_Diff_insert[simp]:
- assumes "finite A" and "a \<in> A" and "a \<notin> B"
+ assumes "a \<in> A" and "a \<notin> 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 \<Longrightarrow> card A \<le> card (insert x A)"
- by (simp add: card_insert_if)
+lemma card_insert_le: "card A \<le> 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 \<Longrightarrow> card (A - {x}) \<le> card A"
- by (cases "x \<in> A") (simp_all add: card_Diff1_less less_imp_le)
+lemma card_Diff1_le: "card (A - {x}) \<le> card A"
+proof (cases "finite A")
+ case True
+ then show ?thesis
+ by (cases "x \<in> A") (simp_all add: card_Diff1_less less_imp_le)
+qed auto
lemma card_psubset: "finite B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> card A < card B \<Longrightarrow> A < B"
by (erule psubsetI) blast
@@ -1833,7 +1845,7 @@
lemma insert_partition:
"x \<notin> F \<Longrightarrow> \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<Longrightarrow> x \<inter> \<Union>F = {}"
- by auto (* somewhat slow *)
+ by auto
lemma finite_psubset_induct [consumes 1, case_names psubset]:
assumes finite: "finite A"
--- a/src/HOL/Library/Disjoint_Sets.thy Fri Sep 03 19:56:03 2021 +0200
+++ b/src/HOL/Library/Disjoint_Sets.thy Fri Sep 03 22:53:11 2021 +0100
@@ -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 (\<Union>P)"
+ shows "partition_on A (insert p P) \<longleftrightarrow> partition_on (A-p) P \<and> p \<subseteq> A \<and> p \<noteq> {}"
+ using assms
+ by (auto simp: partition_on_def disjnt_iff pairwise_insert)
+
subsection \<open>Finiteness of partitions\<close>
lemma finitely_many_partition_on:
--- a/src/HOL/Quotient_Examples/Quotient_FSet.thy Fri Sep 03 19:56:03 2021 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_FSet.thy Fri Sep 03 22:53:11 2021 +0100
@@ -819,8 +819,7 @@
lemma card_remove_fset_le1:
shows "card_fset (remove_fset x xs) \<le> card_fset xs"
- unfolding remove_fset card_fset
- by (rule card_Diff1_le[OF finite_fset])
+ by simp
lemma card_psubset_fset:
shows "ys |\<subseteq>| xs \<Longrightarrow> card_fset ys < card_fset xs \<Longrightarrow> ys |\<subset>| xs"
@@ -835,21 +834,17 @@
lemma card_minus_insert_fset[simp]:
assumes "a |\<in>| A" and "a |\<notin>| 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 |\<subseteq>| 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 |\<inter>| 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 \<open>concat_fset\<close>