src/HOL/Library/Disjoint_Sets.thy

   shows "partition_on (f ` A) ((`) f ` P - {{}})"
 proof (rule partition_on_transform[OF P])
   show "p \<in> P \<Longrightarrow> q \<in> P \<Longrightarrow> disjnt p q \<Longrightarrow> disjnt (f ` p) (f ` q)" for p q
     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:
   assumes "finite A"