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