# 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
```