Theory Graph_Theory.Bidirected_Digraph

theory Bidirected_Digraph
imports
  Digraph
  "HOL-Combinatorics.Permutations"
begin

section ‹Bidirected Graphs›

locale bidirected_digraph = wf_digraph G for G +
  fixes arev :: "'b ⇒ 'b"
  assumes arev_dom: "⋀a. a ∈ arcs G ⟷ arev a ≠ a"
  assumes arev_arev_raw: "⋀a. a ∈ arcs G ⟹ arev (arev a) = a"
  assumes tail_arev[simp]: "⋀a. a ∈ arcs G ⟹ tail G (arev a) = head G a"

lemma (in wf_digraph) bidirected_digraphI:
  assumes arev_eq: "⋀a. a ∉ arcs G ⟹ arev a = a"
  assumes arev_neq: "⋀a. a ∈ arcs G ⟹ arev a ≠ a"
  assumes arev_arev_raw: "⋀a. a ∈ arcs G ⟹ arev (arev a) = a"
  assumes tail_arev: "⋀a. a ∈ arcs G ⟹ tail G (arev a) = head G a"
  shows "bidirected_digraph G arev"
  using assms by unfold_locales (auto simp: permutes_def)

context bidirected_digraph begin

  lemma bidirected_digraph[intro!]: "bidirected_digraph G arev"
    by unfold_locales

  lemma arev_arev[simp]: "arev (arev a) = a"
    using arev_dom by (cases "a ∈ arcs G") (auto simp: arev_arev_raw)

  lemma arev_o_arev[simp]: "arev o arev = id"
    by (simp add: fun_eq_iff)

  lemma arev_eq: "a ∉ arcs G ⟹ arev a = a"
    by (simp add: arev_dom)

  lemma arev_neq: "a ∈ arcs G ⟹ arev a ≠ a"
    by (simp add: arev_dom)

  lemma arev_in_arcs[simp]: "a ∈ arcs G ⟹ arev a ∈ arcs G"
    by (metis arev_arev arev_dom)

  lemma head_arev[simp]:
    assumes "a ∈ arcs G" shows "head G (arev a) = tail G a"
  proof -
    from assms have "head G (arev a) = tail G (arev (arev a)) "
      by (simp only: tail_arev arev_in_arcs)
    then show ?thesis by simp
  qed

  lemma ate_arev[simp]:
    assumes "a ∈ arcs G" shows "arc_to_ends G (arev a) = prod.swap (arc_to_ends G a)"
    using assms by (auto simp: arc_to_ends_def)

  lemma bij_arev: "bij arev"
    using arev_arev by (metis bij_betw_imageI inj_on_inverseI surjI)

  lemma arev_permutes_arcs: "arev permutes arcs G"
    using arev_dom bij_arev by (auto simp: permutes_def bij_iff)

  lemma arev_eq_iff: "⋀x y. arev x = arev y ⟷ x = y"
    by (metis arev_arev)

  lemma in_arcs_eq: "in_arcs G w = arev ` out_arcs G w"
    by auto (metis arev_arev arev_in_arcs image_eqI in_out_arcs_conv tail_arev)

  lemma inj_on_arev[intro!]: "inj_on arev S"
    by (metis arev_arev inj_on_inverseI)

  lemma even_card_loops:
    "even (card (in_arcs G w ∩ out_arcs G w))" (is "even (card ?S)")
  proof -
    { assume "¬finite ?S"
      then have ?thesis by simp
    }
    moreover
    { assume A:"finite ?S"
      have "card ?S = card (⋃{{a,arev a} | a. a ∈ ?S})" (is "_ = card (⋃ ?T)")
        by (rule arg_cong[where f=card]) (auto intro!: exI[where x="{x, arev x}" for x])
      also have "…= sum card ?T"
      proof (rule card_Union_disjoint)
        show "⋀A. A∈{{a, arev a} |a. a ∈ ?S} ⟹ finite A" by auto
        show "pairwise disjnt {{a, arev a} |a. a ∈ in_arcs G w ∩ out_arcs G w}"
          unfolding pairwise_def disjnt_def
           by safe (simp_all add: arev_eq_iff)
      qed
      also have "… = sum (λa. 2) ?T"
        by (intro sum.cong) (auto simp: card_insert_if dest: arev_neq)
      also have "… = 2 * card ?T" by simp
      finally have ?thesis by simp
    }
    ultimately
    show ?thesis by blast
  qed

end

(*XXX*)
sublocale bidirected_digraph ⊆ sym_digraph
proof (unfold_locales, unfold symmetric_def, intro symI)
  fix u v assume "u →⇘G⇙ v"
  then obtain a where "a ∈ arcs G" "arc_to_ends G a = (u,v)" by (auto simp: arcs_ends_def)
  then have "arev a ∈ arcs G" "arc_to_ends G (arev a) = (v,u)"
    by (auto simp: arc_to_ends_def)
  then show "v →⇘G⇙ u" by (auto simp: arcs_ends_def intro: rev_image_eqI)
qed



end