(* Author: Lukas Bulwahn <lukas.bulwahn-at-gmail.com> *) section ‹Combinatorial Basics› theory Injectivity_Solver imports "HOL-Library.Disjoint_Sets" "HOL-Library.Monad_Syntax" "HOL-Eisbach.Eisbach" begin subsection ‹Preliminaries› text ‹ These lemmas shall be added to the Disjoint Set theory. › subsubsection ‹Injectivity and Disjoint Families› lemma inj_on_impl_disjoint_family_on_singleton: assumes "inj_on f A" shows "disjoint_family_on (λx. {f x}) A" using assms disjoint_family_on_def inj_on_contraD by fastforce subsubsection ‹Cardinality Theorems for Set.bind› lemma card_bind: assumes "finite S" assumes "∀X ∈ S. finite (f X)" assumes "disjoint_family_on f S" shows "card (S ⤜ f) = (∑x∈S. card (f x))" proof - have "card (S ⤜ f) = card (⋃(f ` S))" by (simp add: bind_UNION) also have "card (⋃(f ` S)) = (∑x∈S. card (f x))" using assms unfolding disjoint_family_on_def by (simp add: card_UN_disjoint) finally show ?thesis . qed lemma card_bind_constant: assumes "finite S" assumes "∀X ∈ S. finite (f X)" assumes "disjoint_family_on f S" assumes "⋀x. x ∈ S ⟹ card (f x) = k" shows "card (S ⤜ f) = card S * k" using assms by (simp add: card_bind) lemma card_bind_singleton: assumes "finite S" assumes "inj_on f S" shows "card (S ⤜ (λx. {f x})) = card S" using assms by (auto simp add: card_bind_constant inj_on_impl_disjoint_family_on_singleton) subsection ‹Third Version of Injectivity Solver› text ‹ Here, we provide a third version of the injectivity solver. The original first version was provided in the AFP entry `Spivey's Generalized Recurrence for Bell Numbers`. From that method, I derived a second version in the AFP entry `Cardinality of Equivalence Relations`. At roughly the same time, Makarius improved the injectivity solver in the development version of the first AFP entry. This third version now includes the improvements of the second version and Makarius improvements to the first, and it further extends the method to handle the new cases in the cardinality proof of this AFP entry. As the implementation of the injectivity solver only evolves in the development branch of the AFP, the submissions of the three AFP entries that employ the injectivity solver, have to create clones of the injectivity solver for the identified and needed method adjustments. Ultimately, these three clones should only remain in the stable branches of the AFP from Isabelle2016 to Isabelle2017 to work with their corresponding release versions. In the development version, I have now consolidated the three versions here. In the next step, I will move this version of the injectivity solver in the @{theory "HOL-Library.Disjoint_Sets"} and it will hopefully only evolve further there. › lemma disjoint_family_onI: assumes "⋀i j. i ∈ I ∧ j ∈ I ⟹ i ≠ j ⟹ (A i) ∩ (A j) = {}" shows "disjoint_family_on A I" using assms unfolding disjoint_family_on_def by auto lemma disjoint_bind: "⋀S T f g. (⋀s t. S s ∧ T t ⟹ f s ∩ g t = {}) ⟹ ({s. S s} ⤜ f) ∩ ({t. T t} ⤜ g) = {}" by fastforce lemma disjoint_bind': "⋀S T f g. (⋀s t. s ∈ S ∧ t ∈ T ⟹ f s ∩ g t = {}) ⟹ (S ⤜ f) ∩ (T ⤜ g) = {}" by fastforce lemma injectivity_solver_CollectE: assumes "a ∈ {x. P x} ∧ a' ∈ {x. P' x}" assumes "(P a ∧ P' a') ⟹ W" shows "W" using assms by auto lemma injectivity_solver_prep_assms_Collect: assumes "x ∈ {x. P x}" shows "P x ∧ P x" using assms by simp lemma injectivity_solver_prep_assms: "x ∈ A ⟹ x ∈ A ∧ x ∈ A" by simp lemma disjoint_terminal_singleton: "⋀s t X Y. s ≠ t ⟹ (X = Y ⟹ s = t) ⟹ {X} ∩ {Y} = {}" by auto lemma disjoint_terminal_Collect: assumes "s ≠ t" assumes "⋀x x'. S x ∧ T x' ⟹ x = x' ⟹ s = t" shows "{x. S x} ∩ {x. T x} = {}" using assms by auto lemma disjoint_terminal: "s ≠ t ⟹ (⋀x x'. x ∈ S ∧ x' ∈ T ⟹ x = x' ⟹ s = t) ⟹ S ∩ T = {}" by blast lemma elim_singleton: assumes "x ∈ {s} ∧ x' ∈ {t}" obtains "x = s ∧ x' = t" using assms by blast method injectivity_solver uses rule = insert method_facts, use nothing in ‹ ((drule injectivity_solver_prep_assms_Collect | drule injectivity_solver_prep_assms)+)?; rule disjoint_family_onI; ((rule disjoint_bind | rule disjoint_bind')+)?; (erule elim_singleton)?; (erule disjoint_terminal_singleton | erule disjoint_terminal_Collect | erule disjoint_terminal); (elim injectivity_solver_CollectE)?; rule rule; assumption+ › end