Theory Shattering

(*  Title:      Shattering.thy
    Author:     Ata Keskin, TU München
*)

section ‹Definitions and lemmas about shattering›

text ‹In this section, we introduce the predicate @{term "shatters"} and the term for the family of sets that a family shatters @{term "shattered_by"}.›

theory Shattering
  imports Main
begin

subsection ‹Intersection of a family of sets with a set›

abbreviation IntF :: "'a set set ⇒ 'a set ⇒ 'a set set" (infixl ‹∩*› 60)
  where "F ∩* S ≡ ((∩) S) ` F"

lemma idem_IntF:
  assumes "⋃A ⊆ Y"
  shows "A ∩* Y = A"
proof -
  from assms have "A ⊆ A ∩* Y" by blast
  thus ?thesis by fastforce
qed

lemma subset_IntF: 
  assumes "A ⊆ B"
  shows "A ∩* X ⊆ B ∩* X"
  using assms by (rule image_mono)

lemma Int_IntF: "(A ∩* Y) ∩* X = A ∩* (Y ∩ X)"
proof
  show "A ∩* Y ∩* X ⊆ A ∩* (Y ∩ X)"
  proof
    fix S
    assume "S ∈ A ∩* Y ∩* X"
    then obtain a_y where A_Y0: "a_y ∈ A ∩* Y" and A_Y1: "a_y ∩ X = S" by blast
    from A_Y0 obtain a where A0: "a ∈ A" and A1: "a ∩ Y = a_y" by blast
    from A_Y1 A1 have "a ∩ (Y ∩ X) = S" by fast
    with A0 show "S ∈ A ∩* (Y ∩ X)" by blast
  qed
next
  show "A ∩* (Y ∩ X) ⊆ A ∩* Y ∩* X"
  proof
    fix S
    assume "S ∈ A ∩* (Y ∩ X)"
    then obtain a where A0: "a ∈ A" and A1: "a ∩ (Y ∩ X) = S" by blast
    from A0 have "a ∩ Y ∈ A ∩* Y" by blast
    with A1 show "S ∈ (A ∩* Y) ∩* X" by blast
  qed
qed

text ‹@{term insert} distributes over @{term IntF}›
lemma insert_IntF: 
  shows "insert x ` (H ∩* S) = (insert x ` H) ∩* (insert x S)"
proof
  show "insert x ` (H ∩* S) ⊆ (insert x ` H) ∩* (insert x S)"
  proof
    fix y_x
    assume "y_x ∈ insert x ` (H ∩* S)"
    then obtain y where 0: "y ∈ (H ∩* S)" and 1: "y_x = y ∪ {x}" by blast
    from 0 obtain yh where 2: "yh ∈ H" and 3: "y = yh ∩ S" by blast
    from 1 3 have "y_x = (yh ∪ {x}) ∩ (S ∪ {x})" by simp
    with 2 show "y_x ∈ (insert x ` H) ∩* (insert x S)" by blast
  qed
next
  show "insert x ` H ∩* (insert x S) ⊆ insert x ` (H ∩* S)"
  proof
    fix y_x
    assume "y_x ∈ insert x ` H ∩* (insert x S)"
    then obtain yh_x where 0: "yh_x ∈ (λY. Y ∪ {x}) ` H" and 1: "y_x = yh_x ∩ (S ∪ {x})" by blast
    from 0 obtain yh where 2: "yh ∈ H" and 3: "yh_x = yh ∪ {x}" by blast
    from 1 3 have "y_x = (yh ∩ S) ∪ {x}" by simp
    with 2 show "y_x ∈ insert x ` (H ∩* S)" by blast
  qed
qed

subsection ‹Definition of @{term shatters}, @{term VC_dim} and @{term shattered_by}›

abbreviation shatters :: "'a set set ⇒ 'a set ⇒ bool" (infixl ‹shatters› 70)
  where "H shatters A ≡ H ∩* A = Pow A"

definition VC_dim :: "'a set set ⇒ nat"
  where "VC_dim F = Sup {card S | S. F shatters S}"

definition shattered_by :: "'a set set ⇒ 'a set set"
  where "shattered_by F ≡ {A. F shatters A}"

lemma shattered_by_in_Pow:
  shows "shattered_by F ⊆ Pow (⋃ F)"
  unfolding shattered_by_def by blast

lemma subset_shatters:
  assumes "A ⊆ B" and "A shatters X"
  shows "B shatters X"
proof -
  from assms(1) have "A ∩* X ⊆ B ∩* X" by blast
  with assms(2) have "Pow X ⊆ B ∩* X"  by presburger
  thus ?thesis by blast
qed

lemma supset_shatters:
  assumes "Y ⊆ X" and "A shatters X"
  shows "A shatters Y"
proof -
  have h: "⋃(Pow Y) ⊆ Y" by simp
  from assms have 0: "Pow Y ⊆ A ∩* X" by auto
  from subset_IntF[OF 0, of Y] Int_IntF[of Y X A] idem_IntF[OF h] have "Pow Y ⊆ A ∩* (X ∩ Y)" by argo
  with Int_absorb2[OF assms(1)] Int_commute[of X Y] have "Pow Y ⊆ A ∩* Y" by presburger
  then show ?thesis by fast
qed

lemma shatters_empty:
  assumes "F ≠ {}"
  shows "F shatters {}" 
using assms by fastforce

lemma subset_shattered_by:
  assumes "A ⊆ B"
  shows "shattered_by A ⊆ shattered_by B" 
unfolding shattered_by_def using subset_shatters[OF assms] by force

lemma finite_shattered_by:
  assumes "finite (⋃ F)"
  shows "finite (shattered_by F)"
  using assms rev_finite_subset[OF _ shattered_by_in_Pow, of F] by fast

text ‹The following example shows that requiring finiteness of a family of sets is not enough, to ensure that @{term "shattered_by"} also stays finite.›

lemma "∃F::nat set set. finite F ∧ infinite (shattered_by F)"
proof -           
  let ?F = "{odd -` {True}, odd -` {False}}"
  have 0: "finite ?F" by simp

  let ?f = "λn::nat. {n}" 
  let ?N = "range ?f"
  have "inj (λn. {n})" by simp
  with infinite_iff_countable_subset[of ?N] have infinite_N: "infinite ?N" by blast
  have F_shatters_any_singleton: "?F shatters {n::nat}" for n
  proof -
    have Pow_n: "Pow {n} = {{n}, {}}" by blast
    have 1: "Pow {n} ⊆ ?F ∩* {n}" 
    proof (cases "odd n")
      case True
      from True have "(odd -` {False}) ∩ {n} = {}" by blast
      hence 0: "{} ∈ ?F ∩* {n}"  by blast
      from True have "(odd -` {True}) ∩ {n} = {n}" by blast
      hence 1: "{n} ∈ ?F ∩* {n}"  by blast
      from 0 1 Pow_n show ?thesis by simp
    next
      case False
      from False have "(odd -` {True}) ∩ {n} = {}" by blast
      hence 0: "{} ∈ ?F ∩* {n}" by blast
      from False have "(odd -` {False}) ∩ {n} = {n}" by blast
      hence 1: "{n} ∈ ?F ∩* {n}" by blast
      from 0 1 Pow_n show ?thesis by simp
    qed
    thus ?thesis by fastforce
  qed
  then have "?N ⊆ shattered_by ?F" unfolding shattered_by_def by force
  from 0 infinite_super[OF this infinite_N] show ?thesis by blast
qed

end