search

wimmers / poly-reductions

Polynomial-time reductions in Isabelle/HOL
2 stars 13 forks source link

Refactor graph auxiliaries to use `Graph_Theory.Pair_Digraph` #2

Open wimmers opened 4 years ago

wimmers commented 4 years ago

Theory Graph_Auxiliaries restricts graphs to sets of pairs but essentially the same thing is defined in Graph_Theory.Pair_Digraph already, so we should use that instead.

wimmers commented 4 years ago

Now I think we should consider changing everything to the new graph representation to what is under development here: https://github.com/wimmers/archive-of-graph-formalizations

We should definitely discuss this before making the change mentioned above.