[fsgraph] Edge induction principle (fsg_edge_induction)

[binghe]

This PR enriches the fsgraphTheory of finite simple graphs.

Currently there's already the following induction theroem for fsgraph. The idea is to start from empty graph, and then each time adds one node (vertex), together with all new edges connected to it, until the final target graph is constructed:

fsg_induction
⊢ ∀P. P emptyG ∧
      (∀n es g0.
         P g0 ∧ FINITE es ∧ n ∉ nodes g0 ∧
         valid_edges es (n INSERT nodes g0) ∧ (∀e. e ∈ es ⇒ n ∈ e) ⇒
         P (fsgAddEdges es (addNode n () g0))) ⇒
      ∀g. P g

But some graph theory proofs require "edge induction": given a target graph, the induction starts from a graph with the same set of nodes but no edges at all, and each time it adds one edge to the graph, until reaching the final target graph:

fsg_edge_induction
⊢ ∀g P.
    P (fsgAddNodes (nodes g) emptyG) ∧
    (∀g0 x y.
       nodes g0 = nodes g ∧ x ≠ y ∧ {x; y} ⊆ nodes g ∧ {x; y} ∉ fsgedges g0 ∧
       P g0 ⇒
       P (fsgAddEdge x y g0)) ⇒
    P g

where the graph operation for adding just one edge fsgAddEdge is defined (with some supporting theorems):

fsgAddEdge_def
⊢ ∀x y g. fsgAddEdge x y g = addUDEdge x y () g

and the graph operations for adding one node fsgAddNode and a set of nodes `fsgAddNodes:

fsgAddNode_def
⊢ ∀n g. fsgAddNode n g = addNode n () g
fsgAddNodes_def
⊢ ∀N g. fsgAddNodes N g = ITSET fsgAddNode N g

--Chun

[mn200]

I'm not totally against the fsgAddEdge constant, but I'd prefer it to follow the pattern of fsgAddEdges and use the two-element set to represent the edge. You could define it

fsgAddEdge e g0 = fsgAddEdges {e} g0

Given how trivial the above seems, I'm not even sure it's really worth defining.

For the induction principle, I'd use valid_edges {e} (nodes g0) /\ e NOTIN fsgedges g0 to capture the various side-conditions.

[binghe]

Thanks for your comments. I have removed fsgAddEdge and used fsgAddEdges and your suggest statements for the edge induction principle. I found this change actually leads to shorter proofs and shorter theorem statements and this is great.

P. S. It's also possible to remove fsgAddNode n and use only fsgAddNodes {n} instead, but the benefits are not significant.

[mn200]

Thank you for your work on this!