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