theory Eulerian imports "~~/src/HOL/Library/Multiset" begin type_synonym 'node graph = "('node \ 'node) multiset" definition inDegree :: "'node graph \ 'node \ nat" where "inDegree G n = size {# e \# G . snd e = n #}" definition outDegree :: "'node graph \ 'node \ nat" where "outDegree G n = size {# e \# G . fst e = n #}" definition nodes :: "'node graph \ 'node set" where "nodes G = fst ` (set_of G) \ snd ` (set_of G)" inductive path :: "'node graph \ ('node \ 'node) list \ bool" for G :: "'node graph" where ... definition strongly_connected :: "'node graph \ bool" where "strongly_connected G = ..." definition eulerian :: "'node graph \ bool" where "eulerian G = (\es. path G es \ fst (hd es) = snd (last es) \ G = multiset_of es)" theorem eulerian_characterization: "G \ {#} \ eulerian G \ strongly_connected G \ (\v. inDegree G v = outDegree G v)" oops end