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