theory GraphsHW
imports Graphs
begin

lemma path_in_graph:
  assumes dg: "is_digraph G" and p: "is_path G u p v"
  shows "u \<in> V[G] \<and> v \<in> 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) \<in> strongly_connected G"
      from sc dg have "(u,v) \<in> (V[G]) \<times> V[G]"
	unfolding strongly_connected_def
	using path_in_graph by blast
    } hence 1: "strongly_connected G \<subseteq> (V[G]) \<times> V[G]" by auto
    {
      fix v assume vg: "v \<in> V[G]"
      from vg have "is_path G v [] v" by simp
    } hence 2: "\<forall>v\<in>V[G]. (v, v) \<in> 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) \<in> strongly_connected G"
    thus "(v,u) \<in> 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) \<in> strongly_connected G"
      and 2: "(y,z) \<in> 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) \<in> strongly_connected G" 
      unfolding strongly_connected_def by blast
  qed
  from 1 2 3 show ?thesis unfolding equiv_def by blast
qed

end