theory Graphs
imports Main
begin

types vertex = nat
types digraph = "(vertex set) \<times> ((vertex \<times> vertex) set)"

abbreviation vertices :: "digraph \<Rightarrow> vertex set" ("V[_]" [80] 80) where
  "V[G] \<equiv> fst G"
abbreviation edges :: "digraph \<Rightarrow> (vertex \<times> vertex) set" ("E[_]" [80] 80) where
  "E[G] \<equiv> snd G"

definition is_digraph :: "digraph \<Rightarrow> bool" where
  "is_digraph G \<equiv> \<forall> u v. (u,v) \<in> E[G] \<longrightarrow> u \<in> V[G] \<and> v \<in> V[G]"

primrec is_path :: "digraph \<Rightarrow> vertex \<Rightarrow> vertex list \<Rightarrow> vertex \<Rightarrow> bool" where
  "is_path G u [] v = (u \<in> V[G] \<and> u = v)" |
  "is_path G u (v#p) w = ((u,v) \<in> E[G] \<and> is_path G v p w)"

definition strongly_connected :: "digraph \<Rightarrow> (vertex \<times> vertex) set" where
  "strongly_connected G \<equiv> {(u,v). \<exists> p q. is_path G u p v \<and> is_path G v q u}"

theorem strongly_connected_is_equiv:
  assumes dg: "is_digraph G"
  shows "equiv (V[G]) (strongly_connected G)"
  oops

end