theory GraphsHW
imports Graphs
begin
lemma path_in_graph:
assumes dg: "is_digraph G" and p: "is_path G u p v"
shows "u \ V[G] \ v \ V[G]"
using dg p apply (induct p arbitrary: u v)
unfolding is_digraph_def apply force
unfolding is_digraph_def apply force
done
lemma append_path:
assumes xy: "is_path G x p y" and yz: "is_path G y q z"
shows "is_path G x (p@q) z"
using xy yz by (induct p arbitrary: x y z) auto
theorem strongly_connected_is_equiv:
assumes dg: "is_digraph G"
shows "equiv (V[G]) (strongly_connected G)"
proof -
have 1: "refl_on (V[G]) (strongly_connected G)"
proof -
{ fix u v assume sc: "(u,v) \ strongly_connected G"
from sc dg have "(u,v) \ (V[G]) \ V[G]"
unfolding strongly_connected_def
using path_in_graph by blast
} hence 1: "strongly_connected G \ (V[G]) \ V[G]" by auto
{
fix v assume vg: "v \ V[G]"
from vg have "is_path G v [] v" by simp
} hence 2: "\v\V[G]. (v, v) \ strongly_connected G"
unfolding strongly_connected_def by blast
from 1 2 show ?thesis unfolding refl_on_def by blast
qed
have 2: "sym (strongly_connected G)"
unfolding sym_def
proof clarify
fix u v assume "(u,v) \ strongly_connected G"
thus "(v,u) \ strongly_connected G"
unfolding strongly_connected_def by blast
qed
have 3: "trans (strongly_connected G)"
unfolding trans_def
proof clarify
fix x y z assume 1: "(x,y) \ strongly_connected G"
and 2: "(y,z) \ strongly_connected G"
from 1 obtain p1 q1 where xy: "is_path G x p1 y"
and yx: "is_path G y q1 x" unfolding strongly_connected_def by blast
from 2 obtain p2 q2 where yz: "is_path G y p2 z"
and zy: "is_path G z q2 y" unfolding strongly_connected_def by blast
from xy yz have xz: "is_path G x (p1@p2) z" by (rule append_path)
from zy yx have zx: "is_path G z (q2@q1) x" by (rule append_path)
from xz zx show "(x,z) \ strongly_connected G"
unfolding strongly_connected_def by blast
qed
from 1 2 3 show ?thesis unfolding equiv_def by blast
qed
end