Theory Injectivity_Solver

(*  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