diff --git a/metadata/entries/Undirected_Graph_Theory.toml b/metadata/entries/Undirected_Graph_Theory.toml
new file mode 100644
--- /dev/null
+++ b/metadata/entries/Undirected_Graph_Theory.toml
@@ -0,0 +1,44 @@
+title = "Undirected Graph Theory"
+date = 2022-09-29
+topics = [
+ "Mathematics/Graph theory",
+]
+abstract = """
+This entry presents a general library for undirected graph theory -
+enabling reasoning on simple graphs and undirected graphs with loops.
+It primarily is inspired by Noschinski's basic ugraph definition
+in the Girth Chromatic Entry,
+however generalises it in a number of
+ways and significantly expands on the range of basic graph theory
+definitions formalised. Notably, this library removes the constraint
+of vertices being a type synonym with the natural numbers which causes
+issues in more complex mathematical reasoning using graphs, such as
+the Balog Szemeredi Gowers theorem which this library is used for.
+Secondly this library also presents a locale-centric approach,
+enabling more concise, flexible, and reusable modelling of different
+types of graphs. Using this approach enables easy links to be made
+with more expansive formalisations of other combinatorial structures,
+such as incidence systems, as well as various types of formal
+representations of graphs. Further inspiration is also taken from
+Noschinski's Directed Graph library for some proofs and
+definitions on walks, paths and cycles, however these are much
+simplified using the set based representation of graphs, and also
+extended on in this formalisation."""
+license = "bsd"
+note = ""
+
+[authors]
+
+[authors.edmonds]
+homepage = "edmonds_homepage"
+
+[contributors]
+
+[notify]
+edmonds = "edmonds_email"
+
+[history]
+
+[extra]
+
+[related]
diff --git a/thys/ROOTS b/thys/ROOTS
--- a/thys/ROOTS
+++ b/thys/ROOTS
@@ -1,708 +1,709 @@
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
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
Chord_Segments
Circus
Clean
Clique_and_Monotone_Circuits
ClockSynchInst
Closest_Pair_Points
CoCon
CoSMeDis
CoSMed
CofGroups
Coinductive
Coinductive_Languages
Collections
Combinable_Wands
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
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
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
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/Undirected_Graph_Theory/Bipartite_Graphs.thy b/thys/Undirected_Graph_Theory/Bipartite_Graphs.thy
new file mode 100644
--- /dev/null
+++ b/thys/Undirected_Graph_Theory/Bipartite_Graphs.thy
@@ -0,0 +1,407 @@
+theory Bipartite_Graphs imports Undirected_Graph_Walks
+begin
+
+section \Bipartite Graphs \
+
+text \An introductory library for reasoning on bipartite graphs.\
+
+subsection \Bipartite Set Up \
+text \All "edges", i.e. pairs, between any two sets \
+definition all_bi_edges :: "'a set \ 'a set \ 'a edge set" where
+"all_bi_edges X Y \ mk_edge ` (X \ Y)"
+
+lemma all_bi_edges_alt:
+ assumes "X \ Y = {}"
+ shows "all_bi_edges X Y = {e . card e = 2 \ e \ X \ {} \ e \ Y \ {}}"
+ unfolding all_bi_edges_def
+proof (intro subset_antisym subsetI)
+ fix e assume "e \ mk_edge ` (X \ Y)"
+ then obtain v1 v2 where "e = { v1, v2}" and "v1 \ X" and "v2 \ Y"
+ by auto
+ then show "e \ {e. card e = 2 \ e \ X \ {} \ e \ Y \ {}}" using assms
+ using card_2_iff by blast
+next
+ fix e' assume assm: "e' \ {e. card e = 2 \ e \ X \ {} \ e \ Y \ {}}"
+ then obtain v1 where v1in: "v1 \ e'" and "v1 \ X"
+ by blast
+ moreover obtain v2 where v2in: "v2 \ e'" and "v2 \ Y" using assm by blast
+ then have ne: "v1 \ v2"
+ using assms calculation(2) by blast
+ have "card e' = 2" using assm by blast
+ have "{v1, v2} \ e'" using v1in v2in by blast
+ then have "e' = {v1, v2}" using assm v1in v2in
+ by (metis (no_types, opaque_lifting) \card e' = 2\ card_2_iff' insertCI ne subsetI subset_antisym)
+ then show "e' \ mk_edge ` (X \ Y)"
+ by (simp add: \v2 \ Y\ calculation(2) in_mk_edge_img)
+qed
+
+lemma all_bi_edges_alt2: "all_bi_edges X Y = {{x, y} | x y. x \ X \ y \ Y }"
+ unfolding all_bi_edges_def
+proof (intro subset_antisym subsetI)
+ fix x assume "x \ mk_edge ` (X \ Y)"
+ then obtain a b where "(a, b) \ (X \ Y)" and xeq: "x = mk_edge (a, b) " by blast
+ then show "x \ {{x, y} |x y. x \ X \ y \ Y}"
+ by auto
+next
+ fix x assume "x \ {{x, y} |x y. x \ X \ y \ Y}"
+ then obtain a b where xeq: "x = {a, b}" and "a \ X" and "b \ Y"
+ by blast
+ then have "(a, b) \ (X \ Y)" by auto
+ then show "x \ mk_edge ` (X \ Y)" using in_mk_edge_img xeq by metis
+qed
+
+lemma all_bi_edges_wf: "e \ all_bi_edges X Y \ e \ X \ Y"
+ by (auto simp add: all_bi_edges_alt2)
+
+lemma all_bi_edges_2: "X \ Y = {} \ e \ all_bi_edges X Y \ card e = 2"
+ using card_2_iff by (auto simp add: all_bi_edges_alt2)
+
+lemma all_bi_edges_main: "X \ Y = {} \ all_bi_edges X Y \ all_edges (X \ Y)"
+ unfolding all_edges_def using all_bi_edges_wf all_bi_edges_2 by blast
+
+lemma all_bi_edges_finite: "finite X \ finite Y \ finite (all_bi_edges X Y)"
+ by (simp add: all_bi_edges_def)
+
+lemma all_bi_edges_not_ssX: "X \ Y = {} \ e \ all_bi_edges X Y \ \ e \ X"
+ by (auto simp add: all_bi_edges_alt)
+
+lemma all_bi_edges_sym: "all_bi_edges X Y = all_bi_edges Y X"
+ by (auto simp add: all_bi_edges_alt2)
+
+lemma all_bi_edges_not_ssY: "X \ Y = {} \ e \ all_bi_edges X Y \ \ e \ Y"
+ by (auto simp add: all_bi_edges_alt)
+
+lemma card_all_bi_edges:
+ assumes "finite X" "finite Y"
+ assumes "X \ Y = {}"
+ shows "card (all_bi_edges X Y) = card X * card Y"
+proof -
+ have "card (all_bi_edges X Y) = card (X \ Y)"
+ unfolding all_bi_edges_def using inj_on_mk_edge assms card_image by blast
+ thus ?thesis using card_cartesian_product by auto
+qed
+
+lemma (in sgraph) all_edges_between_bi_subset: "mk_edge ` all_edges_between X Y \ all_bi_edges X Y"
+ by (auto simp: all_edges_between_def all_bi_edges_def)
+
+subsection \ Bipartite Graph Locale \
+
+text \For reasoning purposes, it is useful to explicitly label the two sets of vertices as X and Y.
+These are parameters in the locale\
+
+locale bipartite_graph = graph_system +
+ fixes X Y :: "'a set"
+ assumes partition: "partition_on V {X, Y}"
+ assumes ne: "X \ Y"
+ assumes edge_betw: "e \ E \ e \ all_bi_edges X Y"
+begin
+
+lemma part_intersect_empty: "X \ Y = {}"
+ using partition_onD2 partition disjointD ne
+ by blast
+
+lemma X_not_empty: "X \ {}"
+ using partition partition_onD3 by auto
+
+lemma Y_not_empty: "Y \ {}"
+ using partition partition_onD3 by auto
+
+lemma XY_union: "X \ Y = V"
+ using partition partition_onD1 by auto
+
+lemma card_edges_two: "e \ E \ card e = 2"
+ using edge_betw all_bi_edges_alt part_intersect_empty by auto
+
+lemma partitions_ss: "X \ V" "Y \ V"
+ using XY_union by auto
+
+end
+
+text \ By definition, we say an edge must be between X and Y, i.e. contains two vertices \
+sublocale bipartite_graph \ sgraph
+ using card_edges_two by (unfold_locales)
+
+context bipartite_graph
+begin
+
+abbreviation "density \ edge_density X Y"
+
+lemma bipartite_sym: "bipartite_graph V E Y X"
+ using partition ne edge_betw all_bi_edges_sym
+ by (unfold_locales) (auto simp add: insert_commute)
+
+lemma X_verts_not_adj:
+ assumes "x1 \ X" "x2 \ X"
+ shows "\ vert_adj x1 x2"
+proof (rule ccontr, simp add: vert_adj_def)
+ assume "{x1, x2} \ E"
+ then have "\ {x1, x2} \ X"
+ using all_bi_edges_not_ssX edge_betw part_intersect_empty by auto
+ then show False using assms by auto
+qed
+
+lemma Y_verts_not_adj:
+ assumes "y1 \ Y" "y2 \ Y"
+ shows "\ vert_adj y1 y2"
+proof -
+ interpret sym: bipartite_graph V E Y X using bipartite_sym by simp
+ show ?thesis using sym.X_verts_not_adj
+ by (simp add: assms(1) assms(2))
+qed
+
+lemma X_vert_adj_Y: "x \X \ vert_adj x y \ y \ Y"
+ using X_verts_not_adj XY_union vert_adj_imp_inV by blast
+
+lemma Y_vert_adj_X: "y \Y \ vert_adj y x \ x \ X"
+ using Y_verts_not_adj XY_union vert_adj_imp_inV by blast
+
+lemma neighbors_ss_eq_neighborhoodX: "v \ X \ neighborhood v = neighbors_ss v Y"
+ unfolding neighborhood_def neighbors_ss_def
+ by(auto simp add: X_vert_adj_Y vert_adj_imp_inV)
+
+lemma neighbors_ss_eq_neighborhoodY: "v \ Y \ neighborhood v = neighbors_ss v X"
+ unfolding neighborhood_def neighbors_ss_def
+ by(auto simp add: Y_vert_adj_X vert_adj_imp_inV)
+
+lemma neighborhood_subset_oppX: "v \ X \ neighborhood v \ Y"
+ using neighbors_ss_eq_neighborhoodX neighbors_ss_def by auto
+
+lemma neighborhood_subset_oppY: "v \ Y \ neighborhood v \ X"
+ using neighbors_ss_eq_neighborhoodY neighbors_ss_def by auto
+
+lemma degree_neighbors_ssX: "v \ X \ degree v = card (neighbors_ss v Y)"
+ using neighbors_ss_eq_neighborhoodX alt_deg_neighborhood by auto
+
+lemma degree_neighbors_ssY: "v \ Y \ degree v = card (neighbors_ss v X)"
+ using neighbors_ss_eq_neighborhoodY alt_deg_neighborhood by auto
+
+definition is_bicomplete:: "bool" where
+"is_bicomplete \ E = all_bi_edges X Y"
+
+lemma edge_betw_indiv:
+ assumes "e \ E"
+ obtains x y where "x \ X \ y \ Y \ e = {x, y}"
+proof -
+ have "e \ {{x, y} | x y. x \ X \ y \ Y }"
+ using edge_betw all_bi_edges_alt2 assms by blast
+ thus ?thesis
+ using that by auto
+qed
+
+lemma edges_between_equals_edge_set: "mk_edge ` (all_edges_between X Y) = E"
+ by (simp add: all_edges_between_set, intro subset_antisym subsetI, auto) (metis edge_betw_indiv)
+
+text \ Lemmas for reasoning on walks and paths in a bipartite graph \
+lemma walk_alternates:
+ assumes "is_walk w"
+ assumes "Suc i < length w" "i \ 0"
+ shows "w ! i \ X \ w ! (i + 1) \ Y"
+proof -
+ have "{w ! i, w ! (i +1)} \ E" using is_walk_index assms by auto
+ then show ?thesis
+ using X_vert_adj_Y not_vert_adj Y_vert_adj_X vert_adj_sym by blast
+qed
+
+text \A useful reasoning pattern to mimic "wlog" statements for properties that are symmetric
+is to interpret the symmetric bipartite graph and then directly apply the lemma proven earlier\
+lemma walk_alternates_sym:
+ assumes "is_walk w"
+ assumes "Suc i < length w" "i \ 0"
+ shows "w ! i \ Y \ w ! (i + 1) \ X"
+proof -
+ interpret sym: bipartite_graph V E Y X using bipartite_sym by simp
+ show ?thesis using sym.walk_alternates assms by simp
+qed
+
+lemma walk_length_even:
+ assumes "is_walk w"
+ assumes "hd w \ X" and "last w \ X"
+ shows "even (walk_length w)"
+ using assms
+proof (induct "length w" arbitrary: w rule: nat_induct2)
+ case 0
+ then show ?case by (auto simp add: is_walk_def)
+next
+ case 1
+ then have "walk_length w = 0" using walk_length_conv by auto
+ then show ?case by simp
+next
+ case (step n)
+ then show ?case proof (cases "n = 0")
+ case True
+ then have "length w = 2" using step by simp
+ then have "hd w \ X \ last w \ Y" using walk_alternates hd_conv_nth last_conv_nth
+ by (metis add_0 add_diff_cancel_right' less_2_cases_iff list.size(3) nat_1_add_1 step.prems(1)
+ zero_le zero_neq_numeral)
+ then show ?thesis
+ using part_intersect_empty step.prems(2) step.prems(3) by blast
+ next
+ case False
+ have IH: "(\w. n = length w \ is_walk w \ hd w \ X \ last w \ X \ even (walk_length w))"
+ using step by simp
+ obtain w1 w2 where weq: "w = w1@w2" and w1: "w1 = take n w" and w2: "w2 = drop n w"
+ by simp
+ then have ne: "w1 \ []" using False is_walk_not_empty2 step.prems(1) by fastforce
+ then have w1_walk: "is_walk w1" using w1 is_walk_take False
+ by (metis nat_le_linear neq0_conv step.prems(1) take_all)
+ have hdw1: "hd w1 \ X" using step ne weq by auto
+ then have w1n: "length w1 = n" using step length_take w1 by auto
+ then have "length w2 = 2" using step length_drop
+ by (simp add: w2)
+ have "last w = w ! (n + 1)" using step last_conv_nth is_walk_not_empty
+ by (metis add.left_commute diff_add_inverse nat_1_add_1)
+ then have "w ! n \ Y" using step by (simp add: walk_alternates_sym)
+ then have "w ! (n - 1) \ X" using False walk_alternates step by simp
+ then have "last w1 \ X" using step last_conv_nth[of w1] ne w1n
+ by (metis last_list_update list_update_id take_update_swap w1)
+ then have "even (walk_length w1)" using w1_walk w1n hdw1 IH[of w1] by simp
+ then have "even (walk_length w1 + 2)" by simp
+ then show ?thesis using walk_length_conv weq step
+ by (simp add: False w1n)
+ qed
+qed
+
+lemma walk_length_even_sym:
+ assumes "is_walk w"
+ assumes "hd w \ Y"
+ assumes "last w \ Y"
+ shows "even (walk_length w)"
+proof -
+ interpret sym: bipartite_graph V E Y X using bipartite_sym by simp
+ show ?thesis using sym.walk_length_even assms by auto
+qed
+
+lemma walk_length_odd:
+ assumes "is_walk w"
+ assumes "hd w \ X" and "last w \ Y"
+ shows "odd (walk_length w)"
+ using assms
+proof (cases "length w \ 2")
+ case True
+ then have hdin: "hd (tl w) \ Y" using walk_alternates hd_conv_nth
+ by (metis (mono_tags, lifting) Suc_1 Suc_less_eq2 assms(1) assms(2) is_walk_not_empty2 is_walk_tl
+ le_neq_implies_less le_numeral_extra(3) length_greater_0_conv less_Suc_eq nth_tl
+ numeral_1_eq_Suc_0 numerals(1) plus_nat.add_0)
+ have w: "is_walk (tl w)" using assms True is_walk_tl by auto
+ have last: "last (tl w) \ Y" using assms(3) by (simp add: is_walk_not_empty last_tl w)
+ then have ev: "even (walk_length (tl w))" using hdin w walk_length_even_sym[of "tl w"] by auto
+ then have "walk_length w = walk_length (tl w) + 1" using True walk_length_conv by auto
+ then show ?thesis using ev by simp
+next
+ case False
+ have "length w \ 0" using is_walk_not_empty assms by simp
+ then have "length w = 1" using False by linarith
+ then have "hd w = last w"
+ using \length w \ 0\ hd_conv_nth last_conv_nth by fastforce
+ then have "hd w \ X \ last w \ Y" using part_intersect_empty by auto
+ then show ?thesis using assms by simp
+qed
+
+lemma walk_length_odd_sym:
+ assumes "is_walk w"
+ assumes "hd w \ Y" and "last w \ X"
+ shows "odd (walk_length w)"
+proof -
+ interpret sym: bipartite_graph V E Y X using bipartite_sym by simp
+ show ?thesis using assms sym.walk_length_odd by simp
+qed
+
+lemma walk_length_even_iff:
+ assumes "is_walk w"
+ shows "even (walk_length w) \ (hd w \ X \ last w \ X) \ (hd w \ Y \ last w \ Y)"
+proof (intro iffI)
+ assume ev: "even (walk_length w)"
+ show "hd w \ X \ last w \ X \ hd w \ Y \ last w \ Y"
+ proof (rule ccontr)
+ assume "\ ((hd w \ X \ last w \ X) \ (hd w \ Y \ last w \ Y))"
+ then have "(hd w \ X \ last w \ X) \ (hd w \ Y \ last w \ Y)" by simp
+ then have "(hd w \ Y \ last w \ Y) \ (hd w \ X \ last w \ X)" using part_intersect_empty
+ using XY_union assms is_walk_wf_hd is_walk_wf_last by auto
+ then have split: "(hd w \ X \ last w \ Y) \ (hd w \ Y \ last w \ X)"
+ using part_intersect_empty by auto
+ have o1: "(hd w \ X \ last w \ Y) \