# Theory SetUtils

```(*
Auction Theory Toolbox (http://formare.github.io/auctions/)

Authors:
* Marco B. Caminati http://caminati.co.nr
* Manfred Kerber <mnfrd.krbr@gmail.com>
* Christoph Lange <math.semantic.web@gmail.com>
* Colin Rowat <c.rowat@bham.ac.uk>

Dually licenced under
* Creative Commons Attribution (CC-BY) 3.0
(Rationale for this dual licence: http://arxiv.org/abs/1107.3212)
*)

section ‹Additional material that we would have expected in Set.thy›

theory SetUtils
imports
Main

begin

subsection ‹Equality›

text ‹An inference (introduction) rule that combines @{thm equalityI} and @{thm subsetI} to a single step›
lemma equalitySubsetI: "(⋀x . x ∈ A ⟹ x ∈ B) ⟹ (⋀x . x ∈ B ⟹ x ∈ A) ⟹ A = B"
by blast

subsection ‹Trivial sets›

text ‹A trivial set (i.e. singleton or empty), as in Mizar›
definition trivial where "trivial x = (x ⊆ {the_elem x})"

text ‹The empty set is trivial.›
lemma trivial_empty: "trivial {}"
unfolding trivial_def by (rule empty_subsetI)

text ‹A singleton set is trivial.›
lemma trivial_singleton: "trivial {x}"
unfolding trivial_def by simp

text ‹If a trivial set has a singleton subset, the latter is unique.›
lemma singleton_sub_trivial_uniq:
fixes   x X
assumes "{x} ⊆ X" and "trivial X"
shows   "x = the_elem X"
(* CL: The following takes 16 ms in Isabelle2013-1-RC1:
by (metis assms(1) assms(2) insert_not_empty insert_subset subset_empty subset_insert trivial_def trivial_imp_no_distinct) *)
using assms unfolding trivial_def by fast

text ‹Any subset of a trivial set is trivial.›

lemma trivial_subset: fixes X Y assumes "trivial Y" assumes "X ⊆ Y"
shows "trivial X"
(* CL: The following takes 36 ms in Isabelle2013-1-RC1:
by (metis assms(1) assms(2) equals0D no_distinct_imp_trivial subsetI subset_antisym subset_singletonD trivial_cases) *)
using assms unfolding trivial_def
by (metis (full_types) subset_empty subset_insertI2 subset_singletonD)

text ‹There are no two different elements in a trivial set.›

lemma trivial_imp_no_distinct:
assumes triv: "trivial X" and x: "x ∈ X" and y: "y ∈ X"
shows   "x = y"
(* CL: The following takes 17 ms in Isabelle2013-1-RC1: *)
using assms by (metis empty_subsetI insert_subset singleton_sub_trivial_uniq)

subsection ‹The image of a set under a function›

text ‹an equivalent notation for the image of a set, using set comprehension›
lemma image_Collect_mem: "{ f x | x . x ∈ S } = f ` S"
by auto

subsection ‹Big Union›

text ‹An element is in the union of a family of sets if it is in one of the family's member sets.›

lemma Union_member: "(∃ S ∈ F . x ∈ S) ⟷ x ∈ ⋃ F"
by blast

subsection ‹Miscellaneous›

lemma trivial_subset_non_empty: assumes "trivial t" "t ∩ X ≠ {}"
shows   "t ⊆ X"
using trivial_def assms in_mono by fast

lemma trivial_implies_finite: assumes "trivial X"
shows   "finite X"
using assms by (metis finite.simps subset_singletonD trivial_def)
(* finite.simps trivial_cases by metis *)

lemma lm01: assumes "trivial (A × B)"
shows   "(finite (A×B) & card A * (card B) ≤ 1)"
using trivial_def assms One_nat_def card_cartesian_product card.empty card_insert_disjoint
empty_iff finite.emptyI le0 trivial_implies_finite order_refl subset_singletonD by (metis(no_types))

lemma lm02: assumes "finite X"
shows   "trivial X=(card X ≤ 1)"
using assms One_nat_def card.empty card_insert_if card_mono card_seteq empty_iff
empty_subsetI finite.cases finite.emptyI finite_insert insert_mono
trivial_def trivial_singleton
by (metis(no_types))

lemma lm03: shows "trivial {x}"
by (metis order_refl the_elem_eq trivial_def)

lemma lm04: assumes "trivial X" "{x} ⊆ X"
shows   "{x} = X"
using singleton_sub_trivial_uniq assms by (metis subset_antisym trivial_def)

lemma lm05: assumes "¬ trivial X" "trivial T"
shows   "X - T  ≠  {}"
using assms by (metis Diff_iff empty_iff subsetI trivial_subset)

lemma lm06: assumes "(finite (A × B)  &  card A * (card B) ≤ 1)"
shows   "trivial (A × B)"
unfolding trivial_def using trivial_def assms by (metis card_cartesian_product lm02)

lemma lm07: "trivial (A × B) = (finite (A × B) & card A * (card B) ≤ 1)"
using lm01 lm06 by blast

lemma trivial_empty_or_singleton: "trivial X = (X = {} ∨ X = {the_elem X})"
by (metis subset_singletonD trivial_def trivial_empty trivial_singleton)

lemma trivial_cartesian: assumes "trivial X" "trivial Y"
shows   "trivial (X × Y)"
using assms lm07 One_nat_def Sigma_empty1 Sigma_empty2 card.empty card_insert_if
finite_SigmaI trivial_implies_finite nat_1_eq_mult_iff order_refl subset_singletonD trivial_def trivial_empty
by (metis (full_types))

lemma trivial_same: "trivial X = (∀x1 ∈ X. ∀x2 ∈ X. x1 = x2)"
using trivial_def trivial_imp_no_distinct ex_in_conv insertCI subsetI subset_singletonD
trivial_singleton
by (metis (no_types, opaque_lifting))

lemma lm08: assumes "(Pow X ⊆ {{},X})"
shows  "trivial X"
unfolding trivial_same using assms by auto

lemma lm09: assumes "trivial X"
shows "(Pow X ⊆ {{},X})"
using assms trivial_same by fast

lemma lm10: "trivial X = (Pow X ⊆ {{},X})"
using lm08 lm09 by metis

lemma lm11: "({x} × UNIV) ∩ P = {x} × (P `` {x})"
by fast

lemma lm12: "(x,y) ∈ P = (y ∈ P``{x})"
by simp

lemma lm13: assumes "inj_on f A" "inj_on f B"
shows   "inj_on f (A ∪ B)  =  (f`(A-B) ∩ (f`(B-A)) = {})"
using assms inj_on_Un by (metis)

lemma injection_union: assumes "inj_on f A" "inj_on f B" "(f`A) ∩ (f`B) = {}"
shows "inj_on f (A ∪ B)"
using assms lm13 by fast

lemma lm14: "(Pow X = {X}) = (X={})"
by auto

end

```