Support cycle detection in topological_sortTheory

[Gordon-Sau]

• add has_cycle which checks if there are cycles in the graph
• prove that any pair of elements in a partition of the output of the top_sort is connected.
• add predicats TC_depends_on (a TC version of depends_on) and TC_depends_on_weak (which removes the MEM b (MAP FST graph) condition from TC_depends_on)
• prove the correctness of has_cycle (has_cycle_correct and has_cycle_correct2)

[Gordon-Sau]

I am going to add some theorems related to strongly connected components to make it more reusable. The definition of SCC is SCC E x y = RTC E x y /\ RTC E y x.

[mn200]

Thanks for this. The SCC notion feels like it could be moved to relationTheory, but that can be done later.