# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1630689613 -3600
# Node ID 527088d4a89b69db8cd0788e93c4a6d031b90322
# Parent  8798edfc61efb4453c28fc3553dd5f617319306e
strengthened a few lemmas about finite sets and added a code equation for complex_of_real

diff -r 8798edfc61ef -r 527088d4a89b src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Tue Aug 31 13:54:31 2021 +0200
+++ b/src/HOL/Complex.thy	Fri Sep 03 18:20:13 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)
 
diff -r 8798edfc61ef -r 527088d4a89b src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Aug 31 13:54:31 2021 +0200
+++ b/src/HOL/Finite_Set.thy	Fri Sep 03 18:20:13 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"
diff -r 8798edfc61ef -r 527088d4a89b src/HOL/Library/Disjoint_Sets.thy
--- a/src/HOL/Library/Disjoint_Sets.thy	Tue Aug 31 13:54:31 2021 +0200
+++ b/src/HOL/Library/Disjoint_Sets.thy	Fri Sep 03 18:20:13 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: