diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,716 +1,717 @@ 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 Multitape_To_Singletape_TM 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 +Turans_Graph_Theorem 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/Turans_Graph_Theorem/ROOT b/thys/Turans_Graph_Theorem/ROOT new file mode 100644 --- /dev/null +++ b/thys/Turans_Graph_Theorem/ROOT @@ -0,0 +1,12 @@ +chapter AFP + +session Turans_Graph_Theorem (AFP) = "HOL-Probability" + + options [timeout = 600] + sessions + Girth_Chromatic + Random_Graph_Subgraph_Threshold + theories + Turan + document_files + "root.tex" + "root.bib" diff --git a/thys/Turans_Graph_Theorem/Turan.thy b/thys/Turans_Graph_Theorem/Turan.thy new file mode 100644 --- /dev/null +++ b/thys/Turans_Graph_Theorem/Turan.thy @@ -0,0 +1,858 @@ +theory Turan + imports + "Girth_Chromatic.Ugraphs" + "Random_Graph_Subgraph_Threshold.Ugraph_Lemmas" +begin + +section \Basic facts on graphs\ + +lemma wellformed_uverts_0 : + assumes "uwellformed G" and "uverts G = {}" + shows "card (uedges G) = 0" using assms + by (metis uwellformed_def card.empty ex_in_conv zero_neq_numeral) + +lemma finite_verts_edges : + assumes "uwellformed G" and "finite (uverts G)" + shows "finite (uedges G)" +proof - + have sub_pow: "uwellformed G \ uedges G \ {S. S \ uverts G}" + by (cases G, auto simp add: uwellformed_def) + then have "finite {S. S \ uverts G}" using assms + by auto + with sub_pow assms show "finite (uedges G)" + using finite_subset by blast +qed + +lemma ugraph_max_edges : + assumes "uwellformed G" and "card (uverts G) = n" and "finite (uverts G)" + shows "card (uedges G) \ n * (n-1)/2" + using assms wellformed_all_edges [OF assms(1)] card_all_edges [OF assms(3)] Binomial.choose_two [of "card(uverts G)"] + by (smt (verit, del_insts) all_edges_finite card_mono dbl_simps(3) dbl_simps(5) div_times_less_eq_dividend le_divide_eq_numeral1(1) le_square nat_mult_1_right numerals(1) of_nat_1 of_nat_diff of_nat_mono of_nat_mult of_nat_numeral right_diff_distrib') + +lemma subgraph_verts_finite : "\ finite (uverts G); subgraph G' G \ \ finite (uverts G')" + using rev_finite_subset subgraph_def by auto + +section \Cliques\ + +text \In this section a straightforward definition of cliques for simple, undirected graphs is introduced. +Besides fundamental facts about cliques, also more specialized lemmata are proved in subsequent subsections.\ + +definition uclique :: "ugraph \ ugraph \ nat \ bool" where + "uclique C G p \ p = card (uverts C) \ subgraph C G \ C = complete (uverts C)" + +lemma clique_any_edge : + assumes "uclique C G p" and "x \ uverts C" and "y \ uverts C" and "x \ y" + shows "{x,y} \ uedges G" + using assms + apply (simp add: uclique_def complete_def all_edges_def subgraph_def) + by (smt (verit, best) SigmaI fst_conv image_iff mem_Collect_eq mk_uedge.simps snd_conv subset_eq) + +lemma clique_exists : "\ C p. uclique C G p \ p \ card (uverts G)" + using bex_imageD card.empty emptyE gr_implies_not0 le_neq_implies_less + by (auto simp add: uclique_def complete_def subgraph_def all_edges_def) + +lemma clique_exists1 : + assumes "uverts G \ {}" and "finite (uverts G)" + shows "\ C p. uclique C G p \ 0 < p \ p \ card (uverts G)" +proof - + obtain x where x: "x \ uverts G" + using assms + by auto + show ?thesis + apply (rule exI [of _ "({x},{})"], rule exI [of _ 1]) + using x assms(2) + by (simp add: uclique_def subgraph_def complete_def all_edges_def Suc_leI assms(1) card_gt_0_iff) +qed + +lemma clique_max_size : "uclique C G p \ finite (uverts G) \ p \ card (uverts G)" + by (auto simp add: uclique_def subgraph_def Finite_Set.card_mono) + +lemma clique_exists_gt0 : + assumes "finite (uverts G)" "card (uverts G) > 0" + shows "\ C p. uclique C G p \ p \ card (uverts G) \ (\C q. uclique C G q \ q \ p)" +proof - + have 1: "finite (uverts G) \ finite {p. \C. uclique C G p}" + using clique_max_size + by (smt (verit, best) finite_nat_set_iff_bounded_le mem_Collect_eq) + have 2: "\A::nat set. finite A \ \x. x\A \ \x\A.\y\A. y \ x" + using Max_ge Max_in by blast + have "\C p. uclique C G p \ (\C q. uclique C G q \ q \ p)" + using 2 [OF 1 [OF \finite (uverts G)\]] clique_exists [of G] + by (smt (z3) mem_Collect_eq) + then show ?thesis + using \finite (uverts G)\ clique_max_size + by blast +qed + +text \If there exists a $(p+1)$-clique @{term C} in a graph @{term G} + then we can obtain a $p$-clique in @{term G} by removing an arbitrary vertex from @{term C}\ + +lemma clique_size_jumpfree : + assumes "finite (uverts G)" and "uwellformed G" + and "uclique C G (p+1)" + shows "\C'. uclique C' G p" +proof - + have "card(uverts G) > p" + using assms by (simp add: uclique_def subgraph_def card_mono less_eq_Suc_le) + obtain x where x: "x \ uverts C" + using assms by (fastforce simp add: uclique_def) + have "mk_uedge ` {uv \ uverts C \ uverts C. fst uv \ snd uv} - {A \ uedges C. x \ A} = + mk_uedge ` {uv \ (uverts C - {x}) \ (uverts C - {x}). fst uv \ snd uv}" + proof - + have "\y. y \ mk_uedge ` {uv \ uverts C \ uverts C. fst uv \ snd uv} - {A \ uedges C. x \ A} \ + y \ mk_uedge ` {uv \ (uverts C - {x}) \ (uverts C - {x}). fst uv \ snd uv}" + using assms(3) + apply (simp add: uclique_def complete_def all_edges_def) + by (smt (z3) DiffI SigmaE SigmaI image_iff insertCI mem_Collect_eq mk_uedge.simps singleton_iff snd_conv) + moreover have "\y. y \ mk_uedge ` {uv \ (uverts C - {x}) \ (uverts C - {x}). fst uv \ snd uv} + \ y \ mk_uedge ` {uv \ uverts C \ uverts C. fst uv \ snd uv} - {A \ uedges C. x \ A}" + apply (simp add: uclique_def complete_def all_edges_def) + by (smt (z3) DiffE SigmaE SigmaI image_iff insert_iff mem_Collect_eq mk_uedge.simps singleton_iff) + ultimately show ?thesis + by blast + qed + then have 1: "(uverts C - {x}, uedges C - {A \ uedges C. x \ A}) = Ugraph_Lemmas.complete (uverts C - {x})" + using assms(3) + apply (simp add: uclique_def complete_def all_edges_def) + by (metis (no_types, lifting) snd_eqD) + show ?thesis + apply (rule exI [of _ "C -- x"]) + using assms x + apply (simp add: uclique_def remove_vertex_def subgraph_def) + apply (simp add: 1) + by (auto simp add: complete_def all_edges_def) +qed + +text \The next lemma generalises the lemma @{thm [source] clique_size_jumpfree} to a proof of + the existence of a clique of any size smaller than the size of the original clique.\ + +lemma clique_size_decr : + assumes "finite (uverts G)" and "uwellformed G" + and "uclique C G p" + shows "q \ p \ \C. uclique C G q" using assms +proof (induction q rule: measure_induct [of "\x. p - x"]) + case (1 x) + then show ?case + proof (cases "x = p") + case True + then show ?thesis + using \uclique C G p\ + by blast + next + case False + with 1(2) have "x < p" + by auto + from \x < p\ have "p - Suc x < p - x" + by auto + then show ?thesis + using 1(1) assms(1,2,3) \x < p\ + using clique_size_jumpfree [OF \finite (uverts G)\ \uwellformed G\ _] + by (metis "1.prems"(4) add.commute linorder_not_le not_less_eq plus_1_eq_Suc) + qed +qed + +text \With this lemma we can easily derive by contradiction that + if there is no $p$-clique then there cannot exist a clique of a size greater than @{term p}\ + +corollary clique_size_neg_max : + assumes "finite (uverts G)" and "uwellformed G" + and "\(\C. uclique C G p)" + shows "\C q. uclique C G q \ q < p" +proof (rule ccontr) + assume 1: "\ (\C q. uclique C G q \ q < p)" + show False + proof - + obtain C q where C: "uclique C G q" + and q: "q \ p" + using 1 linorder_not_less + by blast + show ?thesis + using assms(3) q clique_size_decr [OF \finite (uverts G)\ \uwellformed G\ C ] + using order_less_imp_le by blast + qed +qed + +corollary clique_complete : + assumes "finite V" and "x \ card V" + shows "\C. uclique C (complete V) x" +proof - + have "uclique (complete V) (complete V) (card V)" + by (simp add: uclique_def complete_def subgraph_def) + then show ?thesis + using clique_size_decr [OF _ complete_wellformed [of V] _ assms(2)] assms(1) + by (simp add: complete_def) +qed + +lemma subgraph_clique : + assumes "uwellformed G" "subgraph C G" "C = complete (uverts C)" + shows "{e \ uedges G. e \ uverts C} = uedges C" +proof - + from assms complete_wellformed [of "uverts C"] have "uedges C \ {e \ uedges G. e \ uverts C}" + by (auto simp add: subgraph_def uwellformed_def) + moreover from assms(1) complete_wellformed [of "uverts C"] have "{e \ uedges G. e \ uverts C} \ uedges C" + apply (simp add: subgraph_def uwellformed_def complete_def card_2_iff all_edges_def) + using assms(3)[unfolded complete_def all_edges_def] in_mk_uedge_img + by (smt (verit, ccfv_threshold) SigmaI fst_conv insert_subset mem_Collect_eq snd_conv subsetI) + ultimately show ?thesis + by auto +qed + +text \Next, we prove that in a graph @{term G} with a $p$-clique @{term C} and some vertex @{term v} outside of this clique, +there exists a $(p+1)$-clique in @{term G} if @{term v} is connected to all nodes in @{term C}. +The next lemma is an abstracted version that does not explicitly mention cliques: +If a vertex @{term n} has as many edges to a set of nodes @{term N} as there are nodes in @{term N} +then @{term n} is connected to all vertices in @{term N}.\ + +lemma card_edges_nodes_all_edges : + fixes G :: "ugraph" and N :: "nat set" and E :: "nat set set" and n :: nat + assumes "uwellformed G" + and "finite N" + and "N \ uverts G" and "E \ uedges G" + and "n \ uverts G" and "n \ N" + and "\e \ E. \x \ N. {n,x} = e" + and "card E = card N" + shows "\x \ N. {n,x} \ E" +proof (rule ccontr) + assume "\(\x \ N. {n,x} \ E)" + show False + proof - + obtain x where x: "x \ N" and e: "{n,x} \ E" + using \\(\x \ N. {n,x} \ E)\ + by auto + have "E \ (\y. {n,y}) ` (N - {x})" + using Set.image_diff_subset \\e \ E. \x \ N. {n,x} = e\ x e + by auto + then show ?thesis + using \finite N\ \card E = card N\ x + using surj_card_le [of "N - {x}" E "(\y. {n,y})"] + by (simp, metis card_gt_0_iff diff_less emptyE lessI linorder_not_le) + qed +qed + +subsection \Partitioning edges along a clique\ + +text \Tur\'{a}n's proof partitions the edges of a graph into three partitions for a $(p-1)$-clique @{term C}: +All edges within @{term C}, all edges outside of @{term C}, and all edges between a vertex in @{term C} and a +vertex not in @{term C}. + +We prove a generalized lemma that partitions the edges along some arbitrary set of vertices +which does not necessarily need to induce a clique. +Furthermore, in Tur\'{a}n's graph theorem we only argue about the cardinality of the partitions +so that we restrict this proof to showing that +the sum of the cardinalities of the partitions is equal to number of all edges.\ + +lemma graph_partition_edges_card : + assumes "finite (uverts G)" and "uwellformed G" and "A \ (uverts G)" + shows "card (uedges G) = card {e \ uedges G. e \ A} + card {e \ uedges G. e \ uverts G - A} + card {e \ uedges G. e \ A \ {} \ e \ (uverts G - A) \ {}}" + using assms +proof - + have "uedges G = {e \ uedges G. e \ A} \ {e \ uedges G. e \ (uverts G) - A} \ {e \ uedges G. e \ A \ {} \ e \ ((uverts G) - A) \ {}}" + using assms uwellformed_def + by blast + moreover have "{e \ uedges G. e \ A} \ {e \ uedges G. e \ uverts G - A} = {}" + using assms uwellformed_def + by (smt (verit, ccfv_SIG) Diff_disjoint Int_subset_iff card.empty disjoint_iff mem_Collect_eq nat.simps(3) nat_1_add_1 plus_1_eq_Suc prod.sel(2) subset_empty) + moreover have "({e \ uedges G. e \ A} \ {e \ uedges G. e \ uverts G - A}) \ {e \ uedges G. e \ A \ {} \ e \ (uverts G - A) \ {}} = {}" + by blast + moreover have "finite {e \ uedges G. e \ A}" using assms + by (simp add: finite_subset) + moreover have "finite {e \ uedges G. e \ uverts G - A}" using assms + by (simp add: finite_subset) + moreover have "finite {e \ uedges G. e \ A \ {} \ e \ (uverts G - A) \ {}}" + using assms finite_verts_edges + by auto + ultimately show ?thesis + using assms Finite_Set.card_Un_disjoint + by (smt (verit, best) finite_UnI) +qed + +text \Now, we turn to the problem of calculating the cardinalities of these partitions +when they are induced by the biggest clique in the graph. + +First, we consider the number of edges in a $p$-clique.\ + +lemma clique_edges_inside : + assumes G1: "uwellformed G" and G2: "finite (uverts G)" + and p: "p \ card (uverts G)" and n: "n = card(uverts G)" + and C: "uclique C G p" + shows "card {e \ uedges G. e \ uverts C} = p * (p-1) / 2" +proof - + have "2 dvd (card (uverts C) * (p - 1))" + using C uclique_def + by auto + have "2 = real 2" + by simp + then show ?thesis + using C uclique_def [of C G p] complete_def [of "uverts C"] + using subgraph_clique [OF G1, of C] subgraph_verts_finite [OF assms(2), of C] + using Real.real_of_nat_div [OF \2 dvd (card (uverts C) * (p - 1))\] Binomial.choose_two [of " card (uverts G)"] + by (smt (verit, del_insts) One_nat_def approximation_preproc_nat(5) card_all_edges diff_self_eq_0 eq_imp_le left_diff_distrib' left_diff_distrib' linorder_not_less mult_le_mono2 n_choose_2_nat not_gr0 not_less_eq_eq of_nat_1 of_nat_diff snd_eqD) +qed + +text \Next, we turn to the number of edges that connect a node inside of the biggest clique with +a node outside of said clique. For that we start by calculating a bound for the number of +edges from one single node outside of the clique into the clique.\ + +lemma clique_edges_inside_to_node_outside : + assumes "uwellformed G" and "finite (uverts G)" + assumes "0 < p" and "p \ card (uverts G)" + assumes "uclique C G p" and "(\C p'. uclique C G p' \ p' \ p)" + assumes y: "y \ uverts G - uverts C" + shows "card {{x,y}| x. x \ uverts C \ {x,y} \ uedges G} \ p - 1" +proof (rule ccontr) + txt \For effective proof automation we use a local function definition to compute this + set of edges into the clique from any node @{term y}:\ + define S where "S \ \y. {{x,y}| x. x \ uverts C \ {x,y} \ uedges G}" + assume "\ card {{x, y} |x. x \ uverts C \ {x, y} \ uedges G} \ p - 1" + then have Sy: "card (S y) > p - 1" + using S_def y by auto + have "uclique ({y} \ (uverts C),S y \ uedges C) G (Suc p)" + proof - + have "card ({y} \ uverts C) = Suc p" + using assms(3,5,7) uclique_def + by (metis DiffD2 card_gt_0_iff card_insert_disjoint insert_is_Un) + moreover have "subgraph ({y} \ uverts C, (S y) \ uedges C) G" + using assms(5,7) + by (auto simp add: uclique_def subgraph_def S_def) + moreover have "({y} \ (uverts C),(S y) \ uedges C) = complete ({y} \ (uverts C))" + proof - + have "(S y) \ uedges C \ all_edges ({y} \ (uverts C))" + using y assms(5) S_def all_edges_def uclique_def complete_def + by (simp, smt (z3) SigmaE SigmaI fst_conv image_iff in_mk_uedge_img insertCI mem_Collect_eq snd_conv subsetI) + moreover have "all_edges ({y} \ (uverts C)) \ (S y) \ uedges C" + proof - + have "\x\uverts C. {y, x} \ S y" + proof - + have "card (S y) = card (uverts C)" + using Sy assms(2,3,5,7) S_def uclique_def card_gt_0_iff + using Finite_Set.surj_card_le [of "uverts C" "S y" "\x. {x, y}"] + by (smt (verit, del_insts) Suc_leI Suc_pred' image_iff le_antisym mem_Collect_eq subsetI) + then show ?thesis + using card_edges_nodes_all_edges [OF assms(1), of "uverts C" "S y" y] assms(1,2,5,7) S_def uclique_def + by (smt (verit, ccfv_threshold) DiffE insert_commute mem_Collect_eq subgraph_def subgraph_verts_finite subsetI) + qed + then show ?thesis + using assms(5) all_edges_def S_def uclique_def complete_def mk_uedge.simps in_mk_uedge_img + by (smt (z3) insert_commute SigmaI fst_conv mem_Collect_eq snd_conv SigmaE UnCI image_iff insert_iff insert_is_Un subsetI) + qed + ultimately show ?thesis + by (auto simp add: complete_def) + qed + ultimately show ?thesis + by (simp add: uclique_def complete_def) + qed + then show False + using assms(6) + by fastforce +qed + +text \Now, that we have this upper bound for the number of edges from a single vertex into the largest clique + we can calculate the upper bound for all such vertices and edges:\ + +lemma clique_edges_inside_to_outside : + assumes G1: "uwellformed G" and G2: "finite (uverts G)" + and p0: "0 < p" and pn: "p \ card (uverts G)" and "card(uverts G) = n" + and C: "uclique C G p" and C_max: "(\C p'. uclique C G p' \ p' \ p)" + shows "card {e \ uedges G. e \ uverts C \ {} \ e \ (uverts G - uverts C) \ {}} \ (p - 1) * (n - p)" +proof - + define S where "S \ \y. {{x,y}| x. x \ uverts C \ {x,y} \ uedges G}" + have "card (uverts G - uverts C) = n - p" + using pn C \card(uverts G) = n\ G2 + apply (simp add: uclique_def) + by (meson card_Diff_subset subgraph_def subgraph_verts_finite) + moreover have "{e \ uedges G. e \ uverts C \ {} \ e \ (uverts G - uverts C) \ {}} = {{x,y}| x y. x \ uverts C \ y \ (uverts G - uverts C) \ {x,y} \ uedges G}" + proof - + have "e \ {e \ uedges G. e \ uverts C \ {} \ e \ (uverts G - uverts C) \ {}} + \ \x y. e = {x,y} \ x \ uverts C \ y \ uverts G - uverts C" for e + using G1 + apply (simp add: uwellformed_def) + by (smt (z3) DiffD2 card_2_iff disjoint_iff_not_equal insert_Diff insert_Diff_if insert_iff) + then show ?thesis + by auto + qed + moreover have "card {{x,y}| x y. x \ uverts C \ y \ (uverts G - uverts C) \ {x,y} \ uedges G} \ card (uverts G - uverts C) * (p-1)" + proof - + have "card {{x,y}| x y. x \ uverts C \ y \ (uverts G - uverts C) \ {x,y} \ uedges G} + \ (\y \ (uverts G - uverts C). card (S y))" + proof - + have "finite (uverts G - uverts C)" + using \finite (uverts G)\ by auto + have "{{x,y}| x y. x \ uverts C \ y \ (uverts G - uverts C) \ {x,y} \ uedges G} + = (\y \ (uverts G - uverts C). {{x,y}| x. x \ uverts C \ {x,y} \ uedges G})" + by auto + then show ?thesis + using Groups_Big.card_UN_le [OF \finite (uverts G - uverts C)\, + of "\y. {{x, y} |x. x \ uverts C \ {x, y} \ uedges G}"] + using S_def + by auto + qed + moreover have "(\y\uverts G - uverts C. card (S y)) \ card (uverts G - uverts C) * (p-1)" + proof - + have "card (S y) \ p - 1" if y: "y \ uverts G - uverts C" for y + using clique_edges_inside_to_node_outside [OF assms(1,2,3,4) C C_max y] S_def y + by simp + then show ?thesis + by (metis id_apply of_nat_eq_id sum_bounded_above) + qed + ultimately show ?thesis + using order_trans + by blast + qed + ultimately show ?thesis + by (smt (verit, ccfv_SIG) mult.commute) +qed + +text \Lastly, we need to argue about the number of edges which are located entirely outside of +the greatest clique. Note that this is in the inductive step case in the overarching proof +of Tur\'{a}n's graph theorem. That is why we have access to the inductive hypothesis as an +assumption in the following lemma:\ + +lemma clique_edges_outside : + assumes "uwellformed G" and "finite (uverts G)" + and p2: "2 \ p" and pn: "p \ card (uverts G)" and n: "n = card(uverts G)" + and C: "uclique C G (p-1)" and C_max: "(\C q. uclique C G q \ q \ p-1)" + and IH: "\G y. y < n \ finite (uverts G) \ uwellformed G \ \C p'. uclique C G p' \ p' < p + \ 2 \ p \ card (uverts G) = y \ real (card (uedges G)) \ (1 - 1 / real (p - 1)) * real (y\<^sup>2) / 2" + shows "card {e \ uedges G. e \ uverts G - uverts C} \ (1 - 1 / (p-1)) * (n - p + 1) ^ 2 / 2" +proof - + have "n - card (uverts C) < n" + using C pn p2 n + by (metis Suc_pred' diff_less less_2_cases_iff linorder_not_less not_gr0 uclique_def) + have GC1: "finite (uverts (uverts G - uverts C, {e \ uedges G. e \ uverts G - uverts C}))" + using assms(2) + by simp + have GC2: "uwellformed (uverts G - uverts C, {e \ uedges G. e \ uverts G - uverts C})" + using assms(1) + by (auto simp add: uwellformed_def) + have GC3: "\C' p'. uclique C' (uverts G - uverts C, {e \ uedges G. e \ uverts G - uverts C}) p' \ p' < p" + proof (rule ccontr) + assume "\(\C' p'. uclique C' (uverts G - uverts C, {e \ uedges G. e \ uverts G - uverts C}) p' \ p' < p)" + then obtain C' p' where C': "uclique C' (uverts G - uverts C, {e \ uedges G. e \ uverts G - uverts C}) p'" and p': "p' \ p" + by auto + then have "uclique C' G p'" + using uclique_def subgraph_def + by auto + then show False + using p' p2 C_max + by fastforce + qed + have GC4: "card (uverts (uverts G - uverts C,{e \ uedges G. e \ uverts G - uverts C})) = n - card (uverts C)" + using C n assms(2) uclique_def subgraph_def + by (simp, meson card_Diff_subset infinite_super) + show ?thesis + using C GC3 IH [OF \n - card (uverts C) < n\ GC1 GC2 GC3 \2 \ p\ GC4] assms(2) n uclique_def + by (simp, smt (verit, best) C One_nat_def Suc_1 Suc_leD clique_max_size of_nat_1 of_nat_diff p2) +qed + +subsection \Extending the size of the biggest clique\ text_raw \\label{sec:extend_clique}\ + +text \In this section, we want to prove that we can add edges to a graph so that we augment the biggest clique +to some greater clique with a specific number of vertices. For that, we need the following lemma: +When too many edges have been added to a graph so that there exists a $(p+1)$-clique +then we can remove at least one of the added edges while also retaining a p-clique\ + +lemma clique_union_size_decr : + assumes "finite (uverts G)" and "uwellformed (uverts G, uedges G \ E)" + and "uclique C (uverts G, uedges G \ E) (p+1)" + and "card E \ 1" + shows "\C' E'. card E' < card E \ uclique C' (uverts G, uedges G \ E') p \ uwellformed (uverts G, uedges G \ E')" +proof (cases "\x \ uverts C. \e \ E. x \ e") + case True + then obtain x where x1: "x \ uverts C" and x2: "\e \ E. x \ e" + by auto + show ?thesis + proof (rule exI [of _ "C -- x"], rule exI [of _ "{e \ E. x \ e}"]) + have "card {e \ E. x \ e} < card E" + using x2 assms(4) + by (smt (verit) One_nat_def card.infinite diff_is_0_eq mem_Collect_eq minus_nat.diff_0 not_less_eq psubset_card_mono psubset_eq subset_eq) + moreover have "uclique (C -- x) (uverts G, uedges G \ {e \ E. x \ e}) p" + proof - + have "p = card (uverts (C -- x))" + using x1 assms(3) + by (auto simp add: uclique_def remove_vertex_def) + moreover have "subgraph (C -- x) (uverts G, uedges G \ {e \ E. x \ e})" + using assms(3) + by (auto simp add: uclique_def subgraph_def remove_vertex_def) + moreover have "C -- x = Ugraph_Lemmas.complete (uverts (C -- x))" + proof - + have 1: "\y. y \ mk_uedge ` {uv \ uverts C \ uverts C. fst uv \ snd uv} - {A \ uedges C. x \ A} \ + y \ mk_uedge ` {uv \ (uverts C - {x}) \ (uverts C - {x}). fst uv \ snd uv}" + by (smt (z3) DiffE DiffI SigmaE SigmaI Ugraph_Lemmas.complete_def all_edges_def assms(3) empty_iff image_iff insert_iff mem_Collect_eq mk_uedge.simps snd_conv uclique_def) + have 2: "\y. y \ mk_uedge ` {uv \ (uverts C - {x}) \ (uverts C - {x}). fst uv \ snd uv} \ + y \ mk_uedge ` {uv \ uverts C \ uverts C. fst uv \ snd uv} - {A \ uedges C. x \ A}" + by (smt (z3) DiffE DiffI SigmaE SigmaI image_iff insert_iff mem_Collect_eq mk_uedge.simps singleton_iff) + show ?thesis + using assms(3) + apply (simp add: remove_vertex_def complete_def all_edges_def uclique_def) + using 1 2 + by (smt (verit, ccfv_SIG) split_pairs subset_antisym subset_eq) + qed + ultimately show ?thesis + by (simp add: uclique_def) + qed + moreover have "uwellformed (uverts G, uedges G \ {e \ E. x \ e})" + using assms(2) + by (auto simp add: uwellformed_def) + ultimately show "card {e \ E. x \ e} < card E \ + uclique (C -- x) (uverts G, uedges G \ {e \ E. x \ e}) p \ + uwellformed (uverts G, uedges G \ {e \ E. x \ e})" + by auto + qed +next + case False + then have "\x. x \ uedges C \ x \ E" + using assms(2) + by (metis assms(3) card_2_iff' complete_wellformed uclique_def uwellformed_def) + then have "uclique C G (p+1)" + using assms(3) + by (auto simp add: uclique_def subgraph_def uwellformed_def) + show ?thesis + using assms(2,4) clique_size_jumpfree [OF assms(1) _ \uclique C G (p+1)\] + apply (simp add: uwellformed_def) + by (metis Suc_le_eq UnCI Un_empty_right card.empty prod.exhaust_sel) +qed + +text \We use this preceding lemma to prove the next result. In this lemma we assume that we have +added too many edges. The goal is then to remove some of the new edges appropriately so +that it is indeed guaranteed that there is no bigger clique. + +Two proofs of this lemma will be described in the following. +Both fundamentally come down to the same core idea: +In essence, both proofs apply the well-ordering principle. +In the first proof we do so immediately by obtaining the minimum of a set:\ + +lemma clique_union_make_greatest : + fixes p n :: nat + assumes "finite (uverts G)" and "uwellformed G" + and "uwellformed (uverts G, uedges G \ E)" and "card(uverts G) \ p" + and "uclique C (uverts G, uedges G \ E) p" + and "\C' q'. uclique C' G q' \ q' < p" and "1 \ card E" + shows "\C' E'. uwellformed (uverts G, uedges G \ E') + \ (uclique C' (uverts G, uedges G \ E') p) + \ (\C'' q'. uclique C'' (uverts G, uedges G \ E') q' \ q' \ p)" + using assms +proof (induction "card E" arbitrary: C E rule: less_induct) + case (less E) + then show ?case + proof (cases "\A. uclique A (uverts G, uedges G \ E) (p+1)") + case True + then obtain A where A: "uclique A (uverts G, uedges G \ E) (p+1)" + by auto + obtain C' E' where E'1: "card E' < card E" + and E'2: "uclique C' (uverts G, uedges G \ E') p" + and E'3: "uwellformed (uverts G, uedges G \ E')" + and E'4: "1 \ card E'" + using less(7) + using clique_union_size_decr [OF assms(1) \uwellformed (uverts G, uedges G \ E)\ A less(8)] + by (metis One_nat_def Suc_le_eq Un_empty_right card_gt_0_iff finite_Un finite_verts_edges fst_conv less.prems(1) less_not_refl prod.collapse snd_conv) + show ?thesis + using less(1) [OF E'1 assms(1,2) E'3 less(5) E'2 less(7) E'4] + using E'1 less(8) + by (meson less_or_eq_imp_le order_le_less_trans) + next + case False + show ?thesis + apply (rule exI [of _ C], rule exI [of _ E]) + using clique_size_neg_max [OF _ less(4) False] + using less(2,4,6) + by fastforce + qed +qed + +text \In this second, alternative proof the well-ordering principle is used through complete induction.\ + +lemma clique_union_make_greatest_alt : + fixes p n :: nat + assumes "finite (uverts G)" and "uwellformed G" + and "uwellformed (uverts G, uedges G \ E)" and "card(uverts G) \ p" + and "uclique C (uverts G, uedges G \ E) p" + and "\C' q'. uclique C' G q' \ q' < p" and "1 \ card E" + shows "\C' E'. uwellformed (uverts G, uedges G \ E') + \ (uclique C' (uverts G, uedges G \ E') p) + \ (\C'' q'. uclique C'' (uverts G, uedges G \ E') q' \ q' \ p)" +proof - + define P where "P \ \E. uwellformed (uverts G, uedges G \ E) \ (\C. uclique C (uverts G, uedges G \ E) p)" + have "finite {y. \E. P E \ card E = y}" + proof - + have "\E. P E \ E \ Pow (uverts G)" + by (auto simp add: P_def uwellformed_def) + then have "finite {E. P E}" + using assms(1) + by (metis Collect_mono Pow_def finite_Pow_iff rev_finite_subset) + then show ?thesis + by simp + qed + obtain F where F1: "P F" + and F2: "card F = Min {y. \E. P E \ card E = y}" + and F3: "card F > 0" + using assms(1,3,4,5,6) Min_in \finite {y. \E. P E \ card E = y}\ P_def CollectD Collect_empty_eq + by (smt (verit, ccfv_threshold) Un_empty_right card_gt_0_iff finite_Un finite_verts_edges fst_conv le_refl linorder_not_le prod.collapse snd_conv) + have "p > 0" + using assms(6) clique_exists bot_nat_0.not_eq_extremum + by blast + then show ?thesis + proof (cases "\C. uclique C (uverts G, uedges G \ F) (p + 1)") + case True + then obtain F' where F'1 : "P F'" and F'2: "card F' < card F" + using F1 F2 F3 clique_union_size_decr [OF assms(1), of F _ p] P_def + by (smt (verit) One_nat_def Suc_eq_plus1 Suc_leI add_2_eq_Suc' assms(1) clique_size_jumpfree fst_conv) + then show ?thesis + using F2 \finite {y. \F. P F \ card F = y}\ Min_gr_iff + by fastforce + next + case False + then show ?thesis + using clique_size_neg_max [OF _ _ False] + using assms(1) F1 P_def + by (smt (verit, ccfv_SIG) Suc_eq_plus1 Suc_leI fst_conv linorder_not_le) + qed +qed + +text \Finally, with this lemma we can turn to this section’s main challenge of increasing the +greatest clique size of a graph by adding edges.\ + +lemma clique_add_edges_max : + fixes p :: nat + assumes "finite (uverts G)" + and "uwellformed G" and "card(uverts G) > p" + and "\C. uclique C G p" and "(\C q'. uclique C G q' \ q' \ p)" + and "q \ card(uverts G)" and "p \ q" + shows "\E. uwellformed (uverts G, uedges G \ E) \ (\C. uclique C (uverts G, uedges G \ E) q) + \ (\C q'. uclique C (uverts G, uedges G \ E) q' \ q' \ q)" +proof (cases "p < q") + case True + then show ?thesis + proof - + have "\E. uwellformed (uverts G, uedges G \ E) \ (\C. uclique C (uverts G, uedges G \ E) q) \ card E \ 1" + apply (rule exI [of _ "all_edges (uverts G)"]) + using Set.Un_absorb1 [OF wellformed_all_edges [OF assms(2)]] + using complete_wellformed [of "uverts G"] clique_complete [OF assms(1,6)] + using all_edges_def assms(1,5) + apply (simp add: complete_def) + by (metis Suc_leI True Un_empty_right all_edges_finite card_gt_0_iff linorder_not_less prod.collapse) + then obtain E C where E1: "uwellformed (uverts G, uedges G \ E)" + and E2: "uclique C (uverts G, uedges G \ E) q" + and E3: "card E \ 1" + by auto + show ?thesis + using clique_union_make_greatest [OF assms(1,2) E1 assms(6) E2 _ E3] assms(5) True + using order_le_less_trans + by blast + qed +next + case False + show ?thesis + apply (rule exI [of _ "{}"]) + using False assms(2,4,5,7) + by simp +qed + +section \Properties of the upper edge bound\ + +text \In this section we prove results about the upper edge bound in Tur\'{a}n's theorem. +The first lemma proves that upper bounds of the sizes of the partitions sum up exactly to the overall upper bound.\ + +lemma turan_sum_eq : + fixes n p :: nat + assumes "p \ 2" and "p \ n" + shows "(p-1) * (p-2) / 2 + (1 - 1 / (p-1)) * (n - p + 1) ^ 2 / 2 + (p - 2) * (n - p + 1) = (1 - 1 / (p-1)) * n^2 / 2" +proof - + have "a * (a-1) / 2 + (1 - 1 / a) * (n - a) ^ 2 / 2 + (a - 1) * (n - a) = (1 - 1 / a) * n^2 / 2" + if a1: "a \ 1" and a2: "n \ a" + for a :: nat + proof - + have "a\<^sup>2 + (n - a)\<^sup>2 + a * (n - a) * 2 = n\<^sup>2" + using a2 + apply (simp flip: Groups.ab_semigroup_mult_class.mult.commute [of 2 "a * (n - a)"]) + apply (simp add: Semiring_Normalization.comm_semiring_1_class.semiring_normalization_rules(18) [of 2 a "(n - a)"]) + by (simp flip: Power.comm_semiring_1_class.power2_sum [of a "n-a"]) + then have "((a - 1) / a) * (a ^ 2 + (n - a) ^ 2 + a * (n - a) * 2) = ((a - 1) / a) * n^2" + by presburger + then have "(((a - 1) / a) * a ^ 2 + ((a - 1) / a) * (n - a) ^ 2 + ((a - 1) / a) * a * (n - a) * 2) = ..." + using Rings.semiring_class.distrib_left [of "(a - 1) / a" "a\<^sup>2 + (n - a)\<^sup>2" "a * (n - a) * 2"] + using Rings.semiring_class.distrib_left [of "(a - 1) / a" "a\<^sup>2" "(n - a)\<^sup>2"] + by auto + moreover have "((a - 1) / a) * a ^ 2 = a * (a-1)" + by (simp add: power2_eq_square) + ultimately have "a * (a-1) + ((a - 1) / a) * (n - a) ^ 2 + (a - 1) * (n - a) * 2 = ((a - 1) / a) * n^2" + using a1 a2 + by auto + moreover have "1 - 1 / a = (a - 1) / a" + by (smt (verit, del_insts) One_nat_def Suc_pred diff_divide_distrib diff_is_0_eq of_nat_1 of_nat_diff of_nat_le_0_iff of_nat_le_iff of_nat_less_iff right_inverse_eq that) + ultimately have "a * (a-1) + (1 - 1 / a) * (n - a) ^ 2 + (a - 1) * (n - a) * 2 = (1 - 1 / a) * n^2" + by simp + then show ?thesis + by simp + qed + moreover have "p - 1 \ 1" + using \p \ 2\ by auto + moreover have "n \ p - 1" + using assms(2) by auto + ultimately show ?thesis + by (smt (verit) assms Nat.add_diff_assoc2 Nat.diff_diff_right diff_diff_left le_eq_less_or_eq less_Suc_eq_le linorder_not_less nat_1_add_1 plus_1_eq_Suc) +qed + +text \The next fact proves that the upper bound of edges is monotonically increasing with the size of the biggest clique.\ + +lemma turan_mono : + fixes n p q :: nat + assumes "0 < q" and "q < p" and "p \ n" + shows "(1 - 1 / q) * n^2 / 2 \ (1 - 1 / (p-1)) * n^2 / 2" + using assms + by (simp add: Extended_Nonnegative_Real.divide_right_mono_ennreal Real.inverse_of_nat_le) + +section \Tur\'{a}n's Graph Theorem\ + +text \In this section we turn to the direct adaptation of Tur\'{a}n's original proof as presented by Aigner and Ziegler \cite{Aigner2018}\ + +theorem turan : + fixes p n :: nat + assumes "finite (uverts G)" + and "uwellformed G" and "\C p'. uclique C G p' \ p' < p" and "p \ 2" and "card(uverts G) = n" + shows "card (uedges G) \ (1 - 1 / (p-1)) * n^2 / 2" using assms +proof (induction n arbitrary: G rule: less_induct) + case (less n) + then show ?case + proof (cases "n < p") + case True + show ?thesis + proof (cases "n") + case 0 + with less True show ?thesis + by (auto simp add: wellformed_uverts_0) + next + case (Suc n') + with True have "(1 - 1 / real n) \ (1 - 1 / real (p - 1))" + by (metis diff_Suc_1 diff_left_mono inverse_of_nat_le less_Suc_eq_le linorder_not_less list_decode.cases not_add_less1 plus_1_eq_Suc) + moreover have "real (card (uedges G)) \ (1 - 1 / real n) * real (n\<^sup>2) / 2" + using ugraph_max_edges [OF less(3,6,2)] + by (smt (verit, ccfv_SIG) left_diff_distrib mult.right_neutral mult_of_nat_commute nonzero_mult_div_cancel_left of_nat_1 of_nat_mult power2_eq_square times_divide_eq_left) + ultimately show ?thesis + using Rings.ordered_semiring_class.mult_right_mono divide_less_eq_numeral1(1) le_less_trans linorder_not_less of_nat_0_le_iff + by (smt (verit, ccfv_threshold) divide_nonneg_nonneg times_divide_eq_right) + qed + next + case False + show ?thesis + proof - + obtain C q where C: "uclique C G q" + and C_max: "(\C q'. uclique C G q' \ q' \ q)" + and q: "q < card (uverts G)" + using clique_exists_gt0 [OF \finite (uverts G)\] False \p \ 2\ less.prems(1,3,5) + by (metis card.empty card_gt_0_iff le_eq_less_or_eq order_less_le_trans pos2) + obtain E C' where E: "uwellformed (uverts G, uedges G \ E)" + and C': "(uclique C' (uverts G, uedges G \ E) (p-1))" + and C'_max: "(\C q'. uclique C (uverts G, uedges G \ E) q' \ q' \ p-1)" + using clique_add_edges_max [OF \finite (uverts G)\ \uwellformed G\ q _ C_max, of "p-1"] + using C less(4) less(5) False \card (uverts G) = n\ + by (smt (verit) One_nat_def Suc_leD Suc_pred less_Suc_eq_le linorder_not_less order_less_le_trans pos2) + have "card {e \ uedges G \ E. e \ uverts C'} = (p-1) * (p-2) / 2" + using clique_edges_inside [OF E _ _ _ C'] False less(2) less.prems(4) C' + by (smt (verit, del_insts) Collect_cong Suc_1 add_leD1 clique_max_size fst_conv of_nat_1 of_nat_add of_nat_diff of_nat_mult plus_1_eq_Suc snd_conv) + moreover have "card {e \ uedges G \ E. e \ uverts G - uverts C'} \ (1 - 1 / (p-1)) * (n - p + 1) ^ 2 / 2" + proof - + have "real(card{e \ uedges (uverts G, uedges G \ E). e \ uverts (uverts G, uedges G \ E) - uverts C'}) + \ (1 - 1 / (real p - 1)) * (real n - real p + 1)\<^sup>2 / 2" + using clique_edges_outside [OF E _ less(5) _ _ C' C'_max, of n] linorder_class.leI [OF False] less(1,2,6) + by (metis (no_types, lifting) fst_conv) + then show ?thesis + by (simp, smt (verit, best) False One_nat_def Suc_1 Suc_leD add.commute leI less.prems(4) of_nat_1 of_nat_diff) + qed + moreover have "card {e \ uedges G \ E. e \ uverts C' \ {} \ e \ (uverts G - uverts C') \ {}} \ (p - 2) * (n - p + 1)" + using clique_edges_inside_to_outside [OF E _ _ _ _ C' C'_max, of n] less(2,5,6) + by (simp, metis (no_types, lifting) C' False Nat.add_diff_assoc Nat.add_diff_assoc2 One_nat_def Suc_1 clique_max_size fst_conv leI mult_Suc_right plus_1_eq_Suc) + ultimately have "real (card (uedges G \ E)) \ (1 - 1 / real (p - 1)) * real (n\<^sup>2) / 2" + using graph_partition_edges_card [OF _ E, of "uverts C'"] + using less(2) turan_sum_eq [OF \2 \ p\, of n] False C' uclique_def subgraph_def + by (smt (verit) Collect_cong fst_eqD linorder_not_le of_nat_add of_nat_mono snd_eqD) + then show ?thesis + using less(2) E finite_verts_edges Finite_Set.card_mono [OF _ Set.Un_upper1 [of "uedges G" E]] + by force + qed + qed +qed + +section \A simplified proof of Tur\'{a}n's Graph Theorem\ + +text \In this section we discuss a simplified proof of Tur\'{a}n's Graph Theorem which uses an idea put forward by the author: +Instead of increasing the size of the biggest clique it is also possible to use the fact that +the expression in Tur\'{a}n's graph theorem is monotonically increasing in the size of the biggest clique (Lemma @{thm [source] turan_mono}). +Hence, it suffices to prove the upper bound for the actual biggest clique size in the graph. +Afterwards, the monotonicity provides the desired inequality. + +The simplifications in the proof are annotated accordingly.\ + +theorem turan' : + fixes p n :: nat + assumes "finite (uverts G)" + and "uwellformed G" and "\C p'. uclique C G p' \ p' < p" and "p \ 2" and "card(uverts G) = n" + shows "card (uedges G) \ (1 - 1 / (p-1)) * n^2 / 2" using assms +proof (induction n arbitrary: p G rule: less_induct) + txt \In the simplified proof we also need to generalize over the biggest clique size @{term p} + so that we can leverage the induction hypothesis in the proof + for the already pre-existing biggest clique size which might be smaller than @{term "p-1"}.\ + case (less n) + then show ?case + proof (cases "n < p") + case True + show ?thesis + proof (cases "n") + case 0 + with less True show ?thesis + by (auto simp add: wellformed_uverts_0) + next + case (Suc n') + with True have "(1 - 1 / real n) \ (1 - 1 / real (p - 1))" + by (metis diff_Suc_1 diff_left_mono inverse_of_nat_le less_Suc_eq_le linorder_not_less list_decode.cases not_add_less1 plus_1_eq_Suc) + moreover have "real (card (uedges G)) \ (1 - 1 / real n) * real (n\<^sup>2) / 2" + using ugraph_max_edges [OF less(3,6,2)] + by (smt (verit, ccfv_SIG) left_diff_distrib mult.right_neutral mult_of_nat_commute nonzero_mult_div_cancel_left of_nat_1 of_nat_mult power2_eq_square times_divide_eq_left) + ultimately show ?thesis + using Rings.ordered_semiring_class.mult_right_mono divide_less_eq_numeral1(1) le_less_trans linorder_not_less of_nat_0_le_iff + by (smt (verit, ccfv_threshold) divide_nonneg_nonneg times_divide_eq_right) + qed + next + case False + show ?thesis + proof - + from False \p \ 2\ + obtain C q where C: "uclique C G q" + and C_max: "(\C q'. uclique C G q' \ q' \ q)" + and q1: "q < card (uverts G)" and q2: "0 < q" + and pq: "q < p" + using clique_exists_gt0 [OF \finite (uverts G)\] clique_exists1 less.prems(1,3,5) + by (metis card.empty card_gt_0_iff le_eq_less_or_eq order_less_le_trans pos2) + txt \In the unsimplified proof we extend this existing greatest clique C to a clique of size @{term "p-1"}. + This part is made superfluous in the simplified proof. + In particular, also Section \ref{sec:extend_clique} is unneeded for this simplified proof. + From here on the proof is analogous to the unsimplified proof + with the potentially smaller clique of size @{term q} in place of the extended clique.\ + have "card {e \ uedges G. e \ uverts C} = q * (q-1) / 2" + using clique_edges_inside [OF less(3,2) _ _ C] q1 less(6) + by auto + moreover have "card {e \ uedges G. e \ uverts G - uverts C} \ (1 - 1 / q) * (n - q) ^ 2 / 2" + proof - + have "real (card {e \ uedges G. e \ uverts G - uverts C}) + \ (1 - 1 / (real (q + 1) - 1)) * (real n - real (q + 1) + 1)\<^sup>2 / 2" + using clique_edges_outside [OF less(3,2) _ _ , of "q+1" n C] C C_max q1 q2 linorder_class.leI [OF False] less(1,6) + by (smt (verit, ccfv_threshold) Suc_1 Suc_eq_plus1 Suc_leI diff_add_inverse2 zero_less_diff) + then show ?thesis + using less.prems(5) q1 + by (simp add: of_nat_diff) + qed + moreover have "card {e \ uedges G. e \ uverts C \ {} \ e \ (uverts G - uverts C) \ {}} \ (q - 1) * (n - q)" + using clique_edges_inside_to_outside [OF less(3,2) q2 _ less(6) C C_max] q1 + by simp + ultimately have "real (card (uedges G)) \ (1 - 1 / real q) * real (n\<^sup>2) / 2" + using graph_partition_edges_card [OF less(2,3), of "uverts C"] + using C uclique_def subgraph_def q1 q2 less.prems(5) turan_sum_eq [of "Suc q" n] + by (smt (verit) Nat.add_diff_assoc Suc_1 Suc_le_eq Suc_le_mono add.commute add.right_neutral diff_Suc_1 diff_Suc_Suc of_nat_add of_nat_mono plus_1_eq_Suc) + then show ?thesis + txt \The final statement can then easily be derived with the monotonicity (Lemma @{thm [source] turan_mono}).\ + using turan_mono [OF q2 pq, of n] False + by linarith + qed + qed +qed + +end diff --git a/thys/Turans_Graph_Theorem/document/root.bib b/thys/Turans_Graph_Theorem/document/root.bib new file mode 100644 --- /dev/null +++ b/thys/Turans_Graph_Theorem/document/root.bib @@ -0,0 +1,22 @@ +@article{turan1941external, + title={On an external problem in graph theory}, + author={Tur{\'a}n, Paul}, + journal={Mat. Fiz. Lapok}, + volume={48}, + pages={436--452}, + year={1941} +} + +@Inbook{Aigner2018, +author="Aigner, Martin +and Ziegler, G{\"u}nter M.", +title="Tur{\'a}n's graph theorem", +bookTitle="Proofs from THE BOOK", +year="2018", +publisher="Springer Berlin Heidelberg", +address="Berlin, Heidelberg", +pages="285--289", +abstract="One of the fundamental results in graph theory is the theorem of Turan from 1941, which initiated extremal graph theory. Turan's theorem was rediscovered many times with various different proofs. We will discuss five of them and let the reader decide which one belongs in The Book.", +isbn="978-3-662-57265-8", +doi="10.1007/978-3-662-57265-8_41", +} \ No newline at end of file diff --git a/thys/Turans_Graph_Theorem/document/root.tex b/thys/Turans_Graph_Theorem/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/Turans_Graph_Theorem/document/root.tex @@ -0,0 +1,75 @@ +\documentclass[11pt,a4paper]{article} +\usepackage[T1]{fontenc} +\usepackage{isabelle,isabellesym} + +% further packages required for unusual symbols (see also +% isabellesym.sty), use only when needed + +%\usepackage{amssymb} + %for \, \, \, \, \, \, + %\, \, \, \, \, + %\, \, \ + +%\usepackage{eurosym} + %for \ + +%\usepackage[only,bigsqcap,bigparallel,fatsemi,interleave,sslash]{stmaryrd} + %for \, \, \, \, \ + +%\usepackage{eufrak} + %for \ ... \, \ ... \ (also included in amssymb) + +%\usepackage{textcomp} + %for \, \, \, \, \, + %\ + +% this should be the last package used +\usepackage{pdfsetup} + +% urls in roman style, theory text in math-similar italics +\urlstyle{rm} +\isabellestyle{it} + +% for uniform font size +%\renewcommand{\isastyle}{\isastyleminor} + + +\begin{document} + +\title{Turán's Graph Theorem} +\author{Nils Lauermann\\ +Computer Laboratory, University of Cambridge CB3 0FD\\ +\texttt{Nils.Lauermann@cl.cam.ac.uk}} +\maketitle + +\begin{abstract} + Turán's Graph Theorem \cite{turan1941external} states that any undirected, simple graph with $n$ vertices that does not contain a $p$-clique, contains at most $\left( 1 - \frac{1}{p-1} \right) \frac{n^2}{2}$ edges. +The theorem is an important result in graph theory and the foundation of the field of extremal graph theory. + +The formalisation follows Aigner and Ziegler's \cite{Aigner2018} presentation of Turán's initial proof \cite{turan1941external}. +Besides a direct adaptation of the textbook proof, a simplified, second proof is presented which decreases the size of the formalised proof significantly. +\end{abstract} + +\tableofcontents + +\subsection*{Acknowledgements} + +This formalisation was developed as part of the author's MPhil dissertation (Submitted on 6 June 2022) of the Advanced Computer Science course at the University of Cambridge. +The project was supervised by Prof Lawrence C. Paulson and Dr Angeliki Koutsoukou-Argyraki. + +\bibliographystyle{abbrv} +\bibliography{root} +\newpage + +% sane default for proof documents +\parindent 0pt\parskip 0.5ex + +% generated text of all theories +\input{session} + +\end{document} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: