diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,714 +1,715 @@ ADS_Functor AI_Planning_Languages_Semantics AODV AVL-Trees AWN Abortable_Linearizable_Modules Abs_Int_ITP2012 Abstract-Hoare-Logics Abstract-Rewriting Abstract_Completeness Abstract_Soundness Ackermanns_not_PR Actuarial_Mathematics Adaptive_State_Counting Affine_Arithmetic Aggregation_Algebras Akra_Bazzi Algebraic_Numbers Algebraic_VCs Allen_Calculus Amicable_Numbers Amortized_Complexity AnselmGod Applicative_Lifting Approximation_Algorithms Architectural_Design_Patterns Aristotles_Assertoric_Syllogistic Arith_Prog_Rel_Primes ArrowImpossibilityGS Attack_Trees Auto2_HOL Auto2_Imperative_HOL AutoFocus-Stream Automated_Stateful_Protocol_Verification Automatic_Refinement AxiomaticCategoryTheory Balog_Szemeredi_Gowers BDD BD_Security_Compositional BNF_CC BNF_Operations BTree Banach_Steinhaus Belief_Revision Bell_Numbers_Spivey BenOr_Kozen_Reif Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate Bicategory BinarySearchTree Binding_Syntax_Theory Binomial-Heaps Binomial-Queues BirdKMP Blue_Eyes Bondy Boolean_Expression_Checkers Boolos_Curious_Inference Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CISC-Kernel CRYSTALS-Kyber CRDT CSP_RefTK CYK CZH_Elementary_Categories CZH_Foundations CZH_Universal_Constructions CakeML CakeML_Codegen Call_Arity Card_Equiv_Relations Card_Multisets Card_Number_Partitions Card_Partitions Cartan_FP Case_Labeling Catalan_Numbers Category Category2 Category3 Cauchy Cayley_Hamilton Certification_Monads Chandy_Lamport CHERI-C_Memory_Model Chord_Segments Circus Clean Clique_and_Monotone_Circuits ClockSynchInst Closest_Pair_Points CoCon CoSMeDis CoSMed CofGroups Coinductive Coinductive_Languages Collections Combinable_Wands Combinatorial_Enumeration_Algorithms Combinatorics_Words Combinatorics_Words_Graph_Lemma Combinatorics_Words_Lyndon Commuting_Hermitian Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Complete_Non_Orders Completeness Complex_Bounded_Operators Complex_Geometry Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Conditional_Simplification Conditional_Transfer_Rule Consensus_Refined Constructive_Cryptography Constructive_Cryptography_CM Constructor_Funs Containers CoreC++ Core_DOM Core_SC_DOM Correctness_Algebras Cotangent_PFD_Formula Count_Complex_Roots CryptHOL CryptoBasedCompositionalProperties Cubic_Quartic_Equations DFS_Framework DOM_Components DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Dedekind_Real Deep_Learning Delta_System_Lemma Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Design_Theory Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic Digit_Expansions Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Dirichlet_L Dirichlet_Series DiscretePricing Discrete_Summation DiskPaxos Dominance_CHK DPRM_Theorem DynamicArchitectures Dynamic_Tables E_Transcendental Echelon_Form EdmondsKarp_Maxflow Efficient-Mergesort Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Equivalence_Relation_Enumeration Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Eval_FO Example-Submission Extended_Finite_State_Machine_Inference Extended_Finite_State_Machines FFT FLP FOL-Fitting FOL_Axiomatic FOL_Harrison FOL_Seq_Calc1 FOL_Seq_Calc2 FOL_Seq_Calc3 FSM_Tests Factor_Algebraic_Polynomial Factored_Transition_System_Bounding Falling_Factorial_Sum Farkas FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite-Map-Extras Finite_Automata_HF Finite_Fields Finitely_Generated_Abelian_Groups First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Fishers_Inequality Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Forcing Formal_Puiseux_Series Formal_SSA Formula_Derivatives Foundation_of_geometry Fourier FO_Theory_Rewriting Free-Boolean-Algebra Free-Groups Frequency_Moments Fresh_Identifiers FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover Furstenberg_Topology GPU_Kernel_PL Gabow_SCC GaleStewart_Games Gale_Shapley Game_Based_Crypto Gauss-Jordan-Elim-Fun Gauss_Jordan Gauss_Sums Gaussian_Integers GenClock General-Triangle Generalized_Counting_Sort Generic_Deriving Generic_Join GewirthPGCProof Girth_Chromatic GoedelGod Goedel_HFSet_Semantic Goedel_HFSet_Semanticless Goedel_Incompleteness Goodstein_Lambda GraphMarkingIBP Graph_Saturation Graph_Theory Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Grothendieck_Schemes Group-Ring-Module HOL-CSP HOLCF-Prelude HRB-Slicing Hahn_Jordan_Decomposition Hales_Jewett Heard_Of Hello_World HereditarilyFinite Hermite Hermite_Lindemann Hidden_Markov_Models Higher_Order_Terms Hoare_Time Hood_Melville_Queue HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL Hyperdual IEEE_Floating_Point IFC_Tracking IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IMP_Compiler IMP_Compiler_Reuse IP_Addresses Imperative_Insertion_Sort Implicational_Logic Impossible_Geometry Incompleteness Incredible_Proof_Machine Independence_CH Inductive_Confidentiality Inductive_Inference InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Interpolation_Polynomials_HOL_Algebra Interpreter_Optimizations Interval_Arithmetic_Word32 Intro_Dest_Elim Involutions2Squares Iptables_Semantics Irrational_Series_Erdos_Straus Irrationality_J_Hancl Irrationals_From_THEBOOK IsaGeoCoq Isabelle_C Isabelle_Marries_Dirac Isabelle_Meta_Model IsaNet Jacobson_Basic_Algebra Jinja JinjaDCI JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Khovanskii_Theorem Kleene_Algebra Knights_Tour Knot_Theory Knuth_Bendix_Order Knuth_Morris_Pratt Koenigsberg_Friendship Kruskal Kuratowski_Closure_Complement LLL_Basis_Reduction LLL_Factorization LOFT LTL LTL_Master_Theorem LTL_Normal_Form LTL_to_DRA LTL_to_GBA Lam-ml-Normalization LambdaAuth LambdaMu Lambda_Free_EPO Lambda_Free_KBOs Lambda_Free_RPOs Lambert_W Landau_Symbols Laplace_Transform Latin_Square LatticeProperties Launchbury Laws_of_Large_Numbers Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option Lifting_the_Exponent LightweightJava LinearQuantifierElim Linear_Inequalities Linear_Programming Linear_Recurrences Liouville_Numbers List-Index List-Infinite List_Interleaving List_Inversions List_Update LocalLexing Localization_Ring Locally-Nameless-Sigma Logging_Independent_Anonymity Lowe_Ontological_Argument Lower_Semicontinuous Lp LP_Duality Lucas_Theorem MDP-Algorithms MDP-Rewards MFMC_Countable MFODL_Monitor_Optimized MFOTL_Monitor MSO_Regex_Equivalence Markov_Models Marriage Mason_Stothers Matrices_for_ODEs Matrix Matrix_Tensor Matroids Maximum_Segment_Sum Max-Card-Matching Median_Method Median_Of_Medians_Selection Menger Mereology Mersenne_Primes Metalogic_ProofChecker MiniML MiniSail Minimal_SSA Minkowskis_Theorem Minsky_Machines Modal_Logics_for_NTS Modular_Assembly_Kit_Security Modular_arithmetic_LLL_and_HNF_algorithms Monad_Memo_DP Monad_Normalisation MonoBoolTranAlgebra MonoidalCategory Monomorphic_Monad MuchAdoAboutTwo Multiset_Ordering_NPC Multi_Party_Computation Multirelations Myhill-Nerode Name_Carrying_Type_Inference Nano_JSON Nash_Williams Nat-Interval-Logic Native_Word Nested_Multisets_Ordinals Network_Security_Policy_Verification Neumann_Morgenstern_Utility No_FTL_observers Nominal2 Noninterference_CSP Noninterference_Concurrent_Composition Noninterference_Generic_Unwinding Noninterference_Inductive_Unwinding Noninterference_Ipurge_Unwinding Noninterference_Sequential_Composition NormByEval Nullstellensatz Number_Theoretic_Transform Octonions OpSets Open_Induction Optics Optimal_BST Orbit_Stabiliser Order_Lattice_Props Ordered_Resolution_Prover Ordinal Ordinal_Partitions Ordinals_and_Cardinals Ordinary_Differential_Equations PAC_Checker Package_logic PAL PAPP_Impossibility PCF PLM POPLmark-deBruijn PSemigroupsConvolution Padic_Ints Padic_Field Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Pell Perfect-Number-Thm Perron_Frobenius Physical_Quantities Pi_Calculus Pi_Transcendental Planarity_Certificates Pluennecke_Ruzsa_Inequality Poincare_Bendixson Poincare_Disc Polynomial_Factorization Polynomial_Interpolation Polynomials Pop_Refinement Posix-Lexing Possibilistic_Noninterference Power_Sum_Polynomials Pratt_Certificate Prefix_Free_Code_Combinators Presburger-Automata Prim_Dijkstra_Simple Prime_Distribution_Elementary Prime_Harmonic_Series Prime_Number_Theorem Priority_Queue_Braun Priority_Search_Trees Probabilistic_Noninterference Probabilistic_Prime_Tests Probabilistic_System_Zoo Probabilistic_Timed_Automata Probabilistic_While Program-Conflict-Analysis Progress_Tracking Projective_Geometry Projective_Measurements Promela Proof_Strategy_Language PropResPI Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem Public_Announcement_Logic QHLProver QR_Decomposition Quantales Quasi_Borel_Spaces Quaternions Query_Optimization Quick_Sort_Cost RIPEMD-160-SPARK ROBDD RSAPSS Ramsey-Infinite Random_BSTs Random_Graph_Subgraph_Threshold Randomised_BSTs Randomised_Social_Choice Rank_Nullity_Theorem Real_Impl Real_Power Real_Time_Deque Recursion-Addition Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Registers Regression_Test_Selection Regular-Sets Regular_Algebras Regular_Tree_Relations Relation_Algebra Relational-Incorrectness-Logic Relational_Disjoint_Set_Forests Relational_Forests Relational_Method Relational_Minimum_Spanning_Trees Relational_Paths Rep_Fin_Groups ResiduatedTransitionSystem Residuated_Lattices Resolution_FOL Rewrite_Properties_Reduction Rewriting_Z Ribbon_Proofs Risk_Free_Lending Robbins-Conjecture Robinson_Arithmetic Root_Balanced_Tree Roth_Arithmetic_Progressions Routing Roy_Floyd_Warshall SATSolverVerification SC_DOM_Components SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 Safe_Distance Safe_OCL Safe_Range_RC Saturation_Framework Saturation_Framework_Extensions +Sauer_Shelah_Lemma SCC_Bloemen_Sequential Schutz_Spacetime Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL Separation_Logic_Unbounded SequentInvertibility Shadow_DOM Shadow_SC_DOM Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Firewall Simplex Simplicial_complexes_and_boolean_functions SimplifiedOntologicalArgument Skew_Heap Skip_Lists Slicing Sliding_Window_Algorithm Smith_Normal_Form Smooth_Manifolds Sophomores_Dream Solidity Sort_Encodings Source_Coding_Theorem SpecCheck Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching Stalnaker_Logic Statecharts Stateful_Protocol_Composition_and_Typing Stellar_Quorums Stern_Brocot Stewart_Apollonius Stirling_Formula Stochastic_Matrices Stone_Algebras Stone_Kleene_Relation_Algebras Stone_Relation_Algebras Store_Buffer_Reduction Stream-Fusion Stream_Fusion_Code Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants Subset_Boolean_Algebras SumSquares Sunflowers SuperCalc Surprise_Paradox Symmetric_Polynomials Syntax_Independent_Logic Szemeredi_Regularity Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Three_Circles Timed_Automata Topological_Semantics Topology TortoiseHare Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Transitive_Models Treaps Tree-Automata Tree_Decomposition Triangle Trie Twelvefold_Way Tycon Types_Tableaus_and_Goedels_God Types_To_Sets_Extension UPF UPF_Firewall UTP Undirected_Graph_Theory Universal_Hash_Families Universal_Turing_Machine UpDown_Scheme Valuation Van_Emde_Boas_Trees Van_der_Waerden VectorSpace VeriComp Verified-Prover Verified_SAT_Based_AI_Planning VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves Virtual_Substitution VolpanoSmith VYDRA_MDL WHATandWHERE_Security WOOT_Strong_Eventual_Consistency WebAssembly Weight_Balanced_Trees Weighted_Arithmetic_Geometric_Mean Weighted_Path_Order Well_Quasi_Orders Wetzels_Problem Winding_Number_Eval Word_Lib WorkerWrapper X86_Semantics XML Youngs_Inequality ZFC_in_HOL Zeta_3_Irrational Zeta_Function pGCL diff --git a/thys/Sauer_Shelah_Lemma/Binomial_Lemmas.thy b/thys/Sauer_Shelah_Lemma/Binomial_Lemmas.thy new file mode 100755 --- /dev/null +++ b/thys/Sauer_Shelah_Lemma/Binomial_Lemmas.thy @@ -0,0 +1,48 @@ +(* Title: Binomial_Lemmas.thy + Author: Ata Keskin, TU München +*) + +section \Lemmas involving the binomial coefficient\ + +text \In this section, we prove lemmas that use the term for the binomial coefficient @{term choose}.\ + +theory Binomial_Lemmas + imports Main +begin + +lemma choose_mono: + assumes "x \ y" + shows "x choose n \ y choose n" +proof - + have "finite {0.. Pow {0.. Pow {0.. Pow {0.. {K \ Pow {0..F)" + shows "card {S. S \ \F \ card S \ k} = (\i\k. card (\ F) choose i)" +proof (induction k) + case 0 + from rev_finite_subset[OF assms] have "S \ \F \ card S \ 0 \ S = {}" for S by fastforce + then show ?case by simp +next + case (Suc k) + let ?FS = "{S. S \ \ F \ card S \ Suc k}" + and ?F_Asm = "{S. S \ \ F \ card S \ k}" + and ?F_Step = "{S. S \ \ F \ card S = Suc k}" + + from finite_Pow_iff[of "\F"] assms have finite_Pow_Un_F: "finite (Pow (\ F))" .. + have "?F_Asm \ Pow (\ F)" and "?F_Step \ Pow (\ F)" by fast+ + with rev_finite_subset[OF finite_Pow_Un_F] have finite_F_Asm: "finite ?F_Asm" and finite_F_Step: "finite ?F_Step" by presburger+ + + have F_Un: "?FS = ?F_Asm \ ?F_Step" and F_disjoint: "?F_Asm \ ?F_Step = {}" by fastforce+ + from card_Un_disjoint[OF finite_F_Asm finite_F_Step F_disjoint] F_Un have "card ?FS = card ?F_Asm + card ?F_Step" by argo + also from Suc have "... = (\i\k. card (\ F) choose i) + card ?F_Step" by argo + also from n_subsets[OF assms, of "Suc k"] have "... = (\i\Suc k. card (\ F) choose i)" by force + finally show ?case by blast +qed + +end \ No newline at end of file diff --git a/thys/Sauer_Shelah_Lemma/Card_Lemmas.thy b/thys/Sauer_Shelah_Lemma/Card_Lemmas.thy new file mode 100755 --- /dev/null +++ b/thys/Sauer_Shelah_Lemma/Card_Lemmas.thy @@ -0,0 +1,55 @@ +(* Title: Card_Lemmas.thy + Author: Ata Keskin, TU München +*) + +section "Lemmas involving the cardinality of sets" + +text \In this section, we prove some lemmas that make use of the term @{term card} or provide bounds for it.\ + +theory Card_Lemmas + imports Main +begin + +lemma card_Int_copy: + assumes "finite X" and "A \ B \ X" and "\f. inj_on f (A \ B) \ (A \ B) \ (f ` (A \ B)) = {} \ f ` (A \ B) \ X" + shows "card A + card B \ card X" +proof - + from rev_finite_subset[OF assms(1), of A] rev_finite_subset[OF assms(1), of B] assms(2) + have finite_A: "finite A" and finite_B: "finite B" by blast+ + then have finite_A_Un_B: "finite (A \ B)" and finite_A_Int_B: "finite (A \ B)" by blast+ + from assms(3) obtain f where f_inj_on: "inj_on f (A \ B)" + and f_disjnt: "(A \ B) \ (f ` (A \ B)) = {}" + and f_imj_in: "f ` (A \ B) \ X" by blast + from finite_A_Int_B have finite_f_img: "finite (f ` (A \ B))" by blast + from assms(2) f_imj_in have union_in: "(A \ B) \ f ` (A \ B) \ X" by blast + + from card_Un_Int[OF finite_A finite_B] have "card A + card B = card (A \ B) + card (A \ B)" . + also from card_image[OF f_inj_on] have "... = card (A \ B) + card (f ` (A \ B))" by presburger + also from card_Un_disjoint[OF finite_A_Un_B finite_f_img f_disjnt] have "... = card ((A \ B) \ f ` (A \ B))" by argo + also from card_mono[OF assms(1) union_in] have "... \ card X" by blast + finally show ?thesis . +qed + +lemma finite_diff_not_empty: + assumes "finite Y" and "card Y < card X" + shows "X - Y \ {}" +proof + assume "X - Y = {}" + hence "X \ Y" by simp + from card_mono[OF assms(1) this] assms(2) show False by linarith +qed + +lemma obtain_difference_element: + fixes F :: "'a set set" + assumes "2 \ card F" + obtains "x" where "x\ \F" "x \ \F" +proof - + from assms card_le_Suc_iff[of 1 F] obtain A F' where 0: "F = insert A F'" and 1: "A \ F'" and 2: "1 \ card F'" by auto + from 2 card_le_Suc_iff[of 0 F'] obtain B F'' where 3: "F' = insert B F''" by auto + from 1 3 have A_noteq_B: "A \ B" by blast + from 0 3 have A_in_F: "A \ F" and B_in_F: "B \ F" by blast+ + from A_noteq_B have "(A - B) \ (B - A) \ {}" by simp + with A_in_F B_in_F that show thesis by blast +qed + +end \ No newline at end of file diff --git a/thys/Sauer_Shelah_Lemma/ROOT b/thys/Sauer_Shelah_Lemma/ROOT new file mode 100755 --- /dev/null +++ b/thys/Sauer_Shelah_Lemma/ROOT @@ -0,0 +1,14 @@ +chapter AFP + +session "Sauer_Shelah_Lemma" (AFP) = HOL + + options [timeout = 600] + + theories + Sauer_Shelah_Lemma + Shattering + Card_Lemmas + Binomial_Lemmas + + document_files + "root.tex" + "root.bib" diff --git a/thys/Sauer_Shelah_Lemma/Sauer_Shelah_Lemma.thy b/thys/Sauer_Shelah_Lemma/Sauer_Shelah_Lemma.thy new file mode 100755 --- /dev/null +++ b/thys/Sauer_Shelah_Lemma/Sauer_Shelah_Lemma.thy @@ -0,0 +1,221 @@ +(* Title: Sauer_Shelah_Lemma.thy + Author: Ata Keskin, TU München +*) + +section "Sauer-Shelah Lemma" + +theory Sauer_Shelah_Lemma + imports Shattering Card_Lemmas Binomial_Lemmas +begin + +subsection \Generalized Sauer-Shelah Lemma\ + +text \To prove the Sauer-Shelah Lemma, we will first prove a slightly stronger fact that every family + @{term "F"} shatters at least as many sets as @{term "card F"}. We first fix an element @{term "x \ (\ F)"} + and consider the subfamily @{term F0} of sets in the family not containing it. By induction, @{term F0} + shatters at least as many elements of @{term F} as @{term "card F0"}. + Next, we consider the subfamily @{term F1} of sets in the family that contain @{term x}. + Again, by induction, @{term F1} shatters as many elements of @{term F} as its cardinality. + The number of elements of @{term F} shattered by @{term F0} and @{term F1} sum up to at least + @{term "card F0 + card F1 = card F"}. When a set @{term "S \ F"} is shattered by only one of the two subfamilies, say @{term F0}, + it contributes one unit to the set @{term "shattered_by F0"} and to @{term "shattered_by F"}. However, when the set is shattered by + both subfamilies, both @{term S} and @{term "S \ {x}"} are in @{term "shattered_by F"}, so @{term S} contributes two units + to @{term "shattered_by F0 \ shattered_by F1"}. Therefore, the cardinality of @{term "shattered_by F"} + is at least equal to the cardinality of @{term "shattered_by F0 \ shattered_by F1"}, which is at least @{term "card F"}.\ + +lemma sauer_shelah_0: + fixes F :: "'a set set" + shows "finite (\ F) \ card F \ card (shattered_by F)" +proof (induction F rule: measure_induct_rule[of "card"]) + case (less F) + note finite_F = finite_UnionD[OF less(2)] + note finite_shF = finite_shattered_by[OF less(2)] + show ?case + proof (cases "2 \ card F") + case True + from obtain_difference_element[OF True] + obtain x :: 'a where x_in_Union_F: "x \ \F" + and x_not_in_Int_F: "x \ \F" by blast + + text \Define F0 as the subfamily of F containing sets that don't contain @{term x}.\ + let ?F0 = "{S \ F. x \ S}" + from x_in_Union_F have F0_psubset_F: "?F0 \ F" by blast + from F0_psubset_F have F0_in_F: "?F0 \ F" by blast + from subset_shattered_by[OF F0_in_F] have shF0_subset_shF: "shattered_by ?F0 \ shattered_by F" . + from F0_in_F have Un_F0_in_Un_F:"\ ?F0 \ \ F" by blast + + text \F0 shatters at least as many sets as @{term "card F0"} by the induction hypothesis.\ + note IH_F0 = less(1)[OF psubset_card_mono[OF finite_F F0_psubset_F] rev_finite_subset[OF less(2) Un_F0_in_Un_F]] + + text \Define F1 as the subfamily of F containing sets that contain @{term x}.\ + let ?F1 = "{S \ F. x \ S}" + from x_not_in_Int_F have F1_psubset_F: "?F1 \ F" by blast + from F1_psubset_F have F1_in_F: "?F1 \ F" by blast + from subset_shattered_by[OF F1_in_F] have shF1_subset_shF: "shattered_by ?F1 \ shattered_by F" . + from F1_in_F have Un_F1_in_Un_F:"\ ?F1 \ \ F" by blast + + text \F1 shatters at least as many sets as @{term "card F1"} by the induction hypothesis.\ + note IH_F1 = less(1)[OF psubset_card_mono[OF finite_F F1_psubset_F] rev_finite_subset[OF less(2) Un_F1_in_Un_F]] + + from shF0_subset_shF shF1_subset_shF + have shattered_subset: "(shattered_by ?F0) \ (shattered_by ?F1) \ shattered_by F" by simp + + text \There is a set with the same cardinality as the intersection of + @{term "shattered_by F0"} and @{term "shattered_by F1"} which is disjoint from their union and is also contained in @{term "shattered_by F"}.\ + have f_copies_the_intersection: + "\f. inj_on f (shattered_by ?F0 \ shattered_by ?F1) \ + (shattered_by ?F0 \ shattered_by ?F1) \ (f ` (shattered_by ?F0 \ shattered_by ?F1)) = {} \ + f ` (shattered_by ?F0 \ shattered_by ?F1) \ shattered_by F" + proof + have x_not_in_shattered: "\S\(shattered_by ?F0) \ (shattered_by ?F1). x \ S" unfolding shattered_by_def by blast + + text \This set is precisely the image of the intersection under @{term "insert x"}.\ + let ?f = "insert x" + have 0: "inj_on ?f (shattered_by ?F0 \ shattered_by ?F1)" + proof + fix X Y + assume x0: "X \ (shattered_by ?F0 \ shattered_by ?F1)" and y0: "Y \ (shattered_by ?F0 \ shattered_by ?F1)" + and 0: "?f X = ?f Y" + from x_not_in_shattered x0 have "X = ?f X - {x}" by blast + also from 0 have "... = ?f Y - {x}" by argo + also from x_not_in_shattered y0 have "... = Y" by blast + finally show "X = Y" . + qed + + text \The set is disjoint from the union.\ + have 1: "(shattered_by ?F0 \ shattered_by ?F1) \ ?f ` (shattered_by ?F0 \ shattered_by ?F1) = {}" + proof (rule ccontr) + assume "(shattered_by ?F0 \ shattered_by ?F1) \ ?f ` (shattered_by ?F0 \ shattered_by ?F1) \ {}" + then obtain S where 10: "S \ (shattered_by ?F0 \ shattered_by ?F1)" + and 11: "S \ ?f ` (shattered_by ?F0 \ shattered_by ?F1)" by auto + from 10 x_not_in_shattered have "x \ S" by blast + with 11 show "False" by blast + qed + + text \This set is also in @{term "shattered_by F"}.\ + have 2: "?f ` (shattered_by ?F0 \ shattered_by ?F1) \ shattered_by F" + proof + fix S_x + assume "S_x \ ?f ` (shattered_by ?F0 \ shattered_by ?F1)" + then obtain S where 20: "S \ shattered_by ?F0" + and 21: "S \ shattered_by ?F1" + and 22: "S_x = ?f S" by blast + from x_not_in_shattered 20 have x_not_in_S: "x \ S" by blast + + from 22 Pow_insert[of x S] have "Pow S_x = Pow S \ ?f ` Pow S" by fast + also from 20 have "... = (?F0 \* S) \ (?f ` Pow S)" unfolding shattered_by_def by blast + also from 21 have "... = (?F0 \* S) \ (?f ` (?F1 \* S))" unfolding shattered_by_def by force + also from insert_IntF[of x S ?F1] have "... = (?F0 \* S) \ (?f ` ?F1 \* (?f S))" by argo + also from 22 have "... = (?F0 \* S) \ (?F1 \* S_x)" by blast + also from 22 have "... = (?F0 \* S_x) \ (?F1 \* S_x)" by blast + also from subset_IntF[OF F0_in_F, of S_x] subset_IntF[OF F1_in_F, of S_x] have "... \ (F \* S_x)" by blast + finally have "Pow S_x \ (F \* S_x)" . + thus "S_x \ shattered_by F" unfolding shattered_by_def by blast + qed + + from 0 1 2 show "inj_on ?f (shattered_by ?F0 \ shattered_by ?F1) \ + (shattered_by ?F0 \ shattered_by ?F1) \ (?f ` (shattered_by ?F0 \ shattered_by ?F1)) = {} \ + ?f ` (shattered_by ?F0 \ shattered_by ?F1) \ shattered_by F" by blast + qed + + have F0_union_F1_is_F: "?F0 \ ?F1 = F" by fastforce + from finite_F have finite_F0: "finite ?F0" and finite_F1: "finite ?F1" by fastforce+ + have disjoint_F0_F1: "?F0 \ ?F1 = {}" by fastforce + + text \We have the following lower bound on the cardinality of @{term "shattered_by F"}:\ + from F0_union_F1_is_F card_Un_disjoint[OF finite_F0 finite_F1 disjoint_F0_F1] + have "card F = card ?F0 + card ?F1" by argo + also from IH_F0 + have "... \ card (shattered_by ?F0) + card ?F1" by linarith + also from IH_F1 + have "... \ card (shattered_by ?F0) + card (shattered_by ?F1)" by linarith + also from card_Int_copy[OF finite_shF shattered_subset f_copies_the_intersection] + have "... \ card (shattered_by F)" by argo + finally show ?thesis . + next + text \If @{term F} contains less than 2 sets, the statement follows trivially.\ + case False + hence "card F = 0 \ card F = 1" by force + thus ?thesis + proof + assume "card F = 0" + thus ?thesis by auto + next + assume asm: "card F = 1" + hence F_not_empty: "F \ {}" by fastforce + from shatters_empty[OF F_not_empty] have "{{}} \ shattered_by F" unfolding shattered_by_def by fastforce + from card_mono[OF finite_shF this] asm show ?thesis by fastforce + qed + qed +qed + +subsection \Sauer-Shelah Lemma\ + +text \The generalized version immediately implies the Sauer-Shelah Lemma, + because only @{text "(\i\k. n choose i)"} of the subsets of an @{term n}-item universe have cardinality less than @{term "k + (1::nat)"}. + Thus, when @{text "(\i\k. n choose i) < card F"}, there are not enough sets to be shattered, + so one of the shattered sets must have cardinality at least @{term "k + (1::nat)"}.\ + +corollary sauer_shelah: + fixes F :: "'a set set" + assumes "finite (\F)" and "(\i\k. card (\F) choose i) < card F" + shows "\S. (F shatters S \ card S = k + 1)" +proof - + let ?K = "{S. S \ \F \ card S \ k}" + from finite_Pow_iff[of F] assms(1) have finite_Pow_Un: "finite (Pow (\F))" by fast + + from sauer_shelah_0[OF assms(1)] assms(2) have "(\i\k. card (\F) choose i) < card (shattered_by F)" by linarith + with choose_row_sum_set[OF assms(1), of k] have "card ?K < card (shattered_by F)" by presburger + + from finite_diff_not_empty[OF finite_subset[OF _ finite_Pow_Un] this] + obtain S where "S \ shattered_by F - ?K" by blast + then have F_shatters_S: "F shatters S" and "S \ \F" and "\(S \ \F \ card S \ k)" unfolding shattered_by_def by blast+ + then have card_S_ge_Suc_k: "k + 1 \ card S" by simp + from obtain_subset_with_card_n[OF card_S_ge_Suc_k] obtain S' where "card S' = k + 1" and "S' \ S" by blast + from this(1) supset_shatters[OF this(2) F_shatters_S] show ?thesis by blast +qed + +subsection \Sauer-Shelah Lemma for hypergraphs\ + +text \If we designate X to be the set of hyperedges and S the set of vertices, we can also formulate the Sauer-Shelah Lemma in terms of hypergraphs. + In this form, the statement provides a sufficient condition for the existence of an hyperedge of a given cardinality which is shattered by the set of edges.\ + +corollary sauer_shelah_2: + fixes X :: "'a set set" and S :: "'a set" + assumes "finite S" and "X \ Pow S" and "(\i\k. card S choose i) < card X" + shows "\Y. (X shatters Y \ card Y = k + 1)" +proof - + from assms(2) have 0: "\X \ S" by blast + then have "(\i\k. card (\X) choose i) \ (\i\k. card S choose i)" + by (simp add: assms(1) card_mono choose_mono sum_mono) + then show ?thesis + using "0" assms finite_subset sauer_shelah by fastforce +qed + +subsection \Alternative statement of the Sauer-Shelah Lemma\ + +text \We can also state the Sauer-Shelah Lemma in terms of the @{term VC_dim}. If the VC-dimension of @{term F} is @{term k} then @{term F} + can consist at most of @{text "(\i\k. card (\F) choose i)"} sets which is in @{text "\(card (\F)^k)"}.\ + +corollary sauer_shelah_alt: + assumes "finite (\F)" and "VC_dim F = k" + shows "card F \ (\i\k. card (\F) choose i)" +proof (rule ccontr) + assume "\ card F \ (\i\k. card (\F) choose i)" hence "(\i\k. card (\F) choose i) < card F" by linarith + then obtain S where "F shatters S" and "card S = k + 1" + by (meson assms(1) sauer_shelah) + then have \
: "k + 1 \ {card S | S. F shatters S}" + by simp metis + have "finite {A. F shatters A}" + by (metis \finite (\ F)\ finite_shattered_by shattered_by_def) + then have "bdd_above {card A |A. F shatters A}" + by simp + then have "k + 1 \ Sup {card A |A. F shatters A}" + by (smt (verit, best) "\
" cSup_upper) + then have "k + 1 \ VC_dim F" + by (simp add: VC_dim_def) + then show False + using assms(2) by auto +qed + +end \ No newline at end of file diff --git a/thys/Sauer_Shelah_Lemma/Shattering.thy b/thys/Sauer_Shelah_Lemma/Shattering.thy new file mode 100755 --- /dev/null +++ b/thys/Sauer_Shelah_Lemma/Shattering.thy @@ -0,0 +1,164 @@ +(* 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 diff --git a/thys/Sauer_Shelah_Lemma/document/root.bib b/thys/Sauer_Shelah_Lemma/document/root.bib new file mode 100644 --- /dev/null +++ b/thys/Sauer_Shelah_Lemma/document/root.bib @@ -0,0 +1,50 @@ +@article{SAUER1972145, +title = {On the density of families of sets}, +journal = {Journal of Combinatorial Theory, Series A}, +volume = {13}, +number = {1}, +pages = {145-147}, +year = {1972}, +issn = {0097-3165}, +doi = {https://doi.org/10.1016/0097-3165(72)90019-2}, +url = {https://www.sciencedirect.com/science/article/pii/0097316572900192}, +author = {N Sauer}, +abstract = {If T is a family of sets and A some set we denote by T ∩ A the following family of subsets of A: T ∩ A = {F ∩ A; F ϵ T}. P. Erdös (oral communication) transmitted to me in Nice the following question: Is it true that if T is a family of subsets of some infinite set S then either there exists to each number n a set A ⊂ S with |A| = n such that |T ∩ A| = 2n or there exists some number N such that |T ∩ A| ⩽ |A|c for each A ⊂ S with |A| ⩾ N and some constant c? In this paper we will answer this question in the affirmative by determining the exact upper bound. (Theorem 2).1} +} + +@article{pjm/1102968432, +author = {Saharon Shelah}, +title = {{A combinatorial problem; stability and order for models and theories in infinitary languages.}}, +volume = {41}, +journal = {Pacific Journal of Mathematics}, +number = {1}, +publisher = {Pacific Journal of Mathematics, A Non-profit Corporation}, +pages = {247 -- 261}, +year = {1972}, +doi = {pjm/1102968432}, +URL = {https://doi.org/} +} + +@misc{kalai_2008, +title={Extremal Combinatorics III: Some Basic Theorems}, +url={https://gilkalai.wordpress.com/2008/09/28/extremal-combinatorics-iii-some-basic-theorems/}, +journal={Combinatorics and more}, +author={Kalai, Gil}, +year={2008}, +month={Sep}} + +@article {MR0288823, + AUTHOR = {Vapnik, V. N. and \v{C}ervonenkis, A. Ja.}, + TITLE = {The uniform convergence of frequencies of the appearance of + events to their probabilities}, + JOURNAL = {Teor. Verojatnost. i Primenen.}, + FJOURNAL = {Akademija Nauk SSSR. Teorija Verojatnoste\u{\i} i ee Primenenija}, + VOLUME = {16}, + YEAR = {1971}, + PAGES = {264--279}, + ISSN = {0040-361x}, + MRCLASS = {60.30}, + MRNUMBER = {0288823}, +MRREVIEWER = {R. M. Dudley}, +} + diff --git a/thys/Sauer_Shelah_Lemma/document/root.tex b/thys/Sauer_Shelah_Lemma/document/root.tex new file mode 100755 --- /dev/null +++ b/thys/Sauer_Shelah_Lemma/document/root.tex @@ -0,0 +1,40 @@ +\documentclass[11pt,a4paper]{article} +\usepackage[T1]{fontenc} +\usepackage{isabelle,isabellesym} + +% this should be the last package used +\usepackage{pdfsetup} + +% urls in roman style, theory text in math-similar italics +\urlstyle{rm} +\isabellestyle{it} + + +\begin{document} + +\title{Sauer-Shelah Lemma} +\author{Ata Keskin} +\maketitle + +\begin{abstract} + The Sauer-Shelah Lemma is a fundamental result in extremal set theory and combinatorics, that guarantees the existence of a set $T$ of size $k$ + which is shattered by a family of sets $\mathcal{F}$, if the cardinality of the family is greater than some bound dependent on $k$. A set $T$ is + said to be shattered by a family $\mathcal{F}$ if every subset of $T$ can be obtained as an intersection of $T$ with some set $S \in \mathcal{F}$. + The Sauer-Shelah Lemma has found use in diverse fields such as computational geometry, approximation algorithms and machine learning. In this entry + we formalize the notion of shattering and prove the generalized and standard versions of the Sauer-Shelah Lemma. +\end{abstract} + +\tableofcontents + +\section{Introduction} + +The goal of this entry is to formalize the Sauer-Shelah Lemma. The result was first published by Sauer \cite{SAUER1972145} and Shelah \cite{pjm/1102968432} independently from one another. The proof presented in this entry is based on an article by Kalai \cite{kalai_2008}. The lemma has a wide range of applications. Vapnik and \v{C}ervonenkis \cite{MR0288823} reproved and used the lemma in the context of statistical learning theory. For instance, the VC-dimension of a family of sets is defined as the size of the largest set the family shatters. In this context, the Sauer-Shelah Lemma is a result tying the VC-dimension of a family to the number of sets in the family. + + +% include generated text of all theories +\input{session} + +\bibliographystyle{abbrv} +\bibliography{root} + +\end{document}