Theory Pair_Graph

theory Pair_Graph
  imports 
    Main
    Graph_Theory.Rtrancl_On
begin

section ‹A Basic Representation of Diraphs›

type_synonym 'v dgraph = "('v × 'v) set"

definition dVs::"('v × 'v) set ⇒ 'v set" where
  "dVs G = ⋃ {{v1,v2} | v1 v2. (v1, v2) ∈ G}"

lemma induct_pcpl:
  "⟦P []; ⋀x. P [x]; ⋀x y zs. P zs ⟹ P (x # y # zs)⟧ ⟹ P xs"
  by induction_schema (pat_completeness, lexicographic_order)

lemma induct_pcpl_2:
  "⟦P []; ⋀x. P [x]; ⋀x y. P [x,y]; ⋀x y z. P [x,y,z]; ⋀w x y z zs. P zs ⟹ P (w # x # y # z # zs)⟧ ⟹ P xs"
  by induction_schema (pat_completeness, lexicographic_order)

lemma dVs_empty[simp]: "dVs {} = {}"
  by (simp add: dVs_def)

lemma dVs_empty_iff[simp]: "dVs E = {} ⟷ E = {}"
  unfolding dVs_def by auto

lemma dVsI[intro]:
  assumes "(a, v) ∈ dG" shows "a ∈ dVs dG" and "v ∈ dVs dG"
  using assms unfolding dVs_def by auto

lemma dVsI':
  assumes "e ∈ dG" shows "fst e ∈ dVs dG" and "snd e ∈ dVs dG"
  using assms
  by (auto intro: dVsI[of "fst e" "snd e"])

lemma dVs_union_distr[simp]: "dVs (G ∪ H) = dVs G ∪ dVs H"
  unfolding dVs_def by blast

lemma dVs_union_big_distr: "dVs (⋃G) = ⋃(dVs ` G)"
  apply (induction G rule: infinite_finite_induct)
  apply simp_all
  by (auto simp add: dVs_def)

lemma dVs_eq: "dVs E = fst ` E ∪ snd ` E"
  by (induction E rule: infinite_finite_induct)
     (auto simp: dVs_def intro!: image_eqI, blast+)

lemma finite_vertices_iff: "finite (dVs E) ⟷ finite E" (is "?L ⟷ ?R")
proof
  show "?R ⟹ ?L"
    by (induction E rule: finite_induct)
       (auto simp: dVs_eq)
  show "?L ⟹ ?R"
  proof (rule ccontr)
    show "?L ⟹ ¬?R ⟹ False"
      unfolding dVs_eq
      using finite_subset subset_fst_snd by fastforce
  qed
qed

abbreviation reachable1 :: "('v × 'v) set ⇒ 'v ⇒ 'v ⇒ bool" ("_ →⇧+ı _" [100,100] 40) where
  "reachable1 E u v ≡ (u,v) ∈ E⇧+"

definition reachable :: "('v × 'v) set ⇒ 'v ⇒ 'v ⇒ bool" ("_ →⇧*ı _" [100,100] 40) where
  "reachable E u v = ( (u,v) ∈ rtrancl_on (dVs E) E)"

lemma reachableE[elim?]:
  assumes "(u,v) ∈ E"
  obtains e where "e ∈ E" "e = (u, v)"
  using assms by auto

lemma reachable_refl[intro!, Pure.intro!, simp]: "v ∈ dVs E ⟹ v →⇧*⇘E⇙ v"
  unfolding reachable_def by auto

lemma reachable_trans[trans,intro]:
  assumes "u →⇧*⇘E⇙ v" "v →⇧*⇘E⇙ w" shows "u →⇧*⇘E⇙ w"
  using assms unfolding reachable_def by (rule rtrancl_on_trans)

lemma reachable_edge[dest,intro]: "(u,v) ∈ E ⟹ u →⇧*⇘E⇙ v"
  unfolding reachable_def
  by (auto intro!: rtrancl_consistent_rtrancl_on)

lemma reachable_induct[consumes 1, case_names base step]:
  assumes major: "u →⇧*⇘E⇙ v"
    and cases: "⟦u ∈ dVs E⟧ ⟹ P u"
      "⋀x y. ⟦u →⇧*⇘E⇙ x; (x,y) ∈ E; P x⟧ ⟹ P y"
  shows "P v"
  using assms unfolding reachable_def by (rule rtrancl_on_induct)

lemma converse_reachable_induct[consumes 1, case_names base step, induct pred: reachable]:
  assumes major: "u →⇧*⇘E⇙ v"
    and cases: "v ∈ dVs E ⟹ P v"
      "⋀x y. ⟦(x,y) ∈ E; y →⇧*⇘E⇙ v; P y⟧ ⟹ P x"
    shows "P u"
  using assms unfolding reachable_def by (rule converse_rtrancl_on_induct)

lemma reachable_in_dVs:
  assumes "u →⇧*⇘E⇙ v"
  shows "u ∈ dVs E" "v ∈ dVs E"
  using assms by (induct) (simp_all add: dVsI)

lemma reachable1_in_dVs:
  assumes "u →⇧+⇘E⇙ v"
  shows "u ∈ dVs E" "v ∈ dVs E"
  using assms by (induct) (simp_all add: dVsI)

lemma reachable1_reachable[intro]:
  "v →⇧+⇘E⇙ w ⟹ v →⇧*⇘E⇙ w"
  unfolding reachable_def
  by (auto intro: rtrancl_consistent_rtrancl_on simp: dVsI reachable1_in_dVs)

lemmas reachable1_reachableE[elim] = reachable1_reachable[elim_format]

lemma reachable_neq_reachable1[intro]:
  assumes reach: "v →⇧*⇘E⇙ w"
    and neq: "v ≠ w"
  shows "v →⇧+⇘E⇙ w" 
  using assms
  unfolding reachable_def
  by (auto dest: rtrancl_on_rtranclI rtranclD)

lemmas reachable_neq_reachable1E[elim] = reachable_neq_reachable1[elim_format]

lemma arc_implies_dominates: "e ∈ E ⟹ (fst e, snd e) ∈ E" by auto

definition neighbourhood::"('v × 'v) set ⇒ 'v ⇒ 'v set" where
  "neighbourhood G u = {v. (u,v) ∈ G}"

lemma 
  neighbourhoodI[intro]: "v ∈ (neighbourhood G u) ⟹ (u,v) ∈ G" and
  neighbourhoodD[dest]: "(u,v) ∈ G ⟹ v ∈ (neighbourhood G u)"
  by (auto simp: neighbourhood_def)


definition "sources G = {u | u v . (u,v) ∈ G}"

definition "sinks G = {v | u v . (u,v) ∈ G}"

lemma dVs_subset: "G ⊆ G' ⟹ dVs G ⊆ dVs G'"
  by (auto simp: dVs_def)

lemma dVs_insert[elim]:
  "v∈ dVs (insert (x,y) G) ⟹ ⟦v = x ⟹ P; v = y ⟹ P; v ∈ dVs G ⟹ P⟧ ⟹ P"
  by (auto simp: dVs_def)

lemma in_neighbourhood_dVs[simp, intro]:
  "v ∈ neighbourhood G u ⟹ v ∈ dVs G"
  by auto

lemma subset_neighbourhood_dVs[simp, intro]:
  "neighbourhood G u ⊆ dVs G"
  by auto

lemma in_dVsE: "v ∈ dVs G ⟹ ⟦(⋀u. (u, v) ∈ G ⟹ P); (⋀u. (v, u) ∈ G ⟹ P)⟧ ⟹ P"
               "v ∉ dVs G ⟹ (⟦(⋀u. (u, v) ∉ G); (⋀u. (v, u) ∉ G)⟧ ⟹ P) ⟹ P"
  by (auto simp: dVs_def)

lemma neighoubrhood_union[simp]: "neighbourhood (G ∪ G') u = neighbourhood G u ∪ neighbourhood G' u"
  by (auto simp: neighbourhood_def)

lemma vs_are_gen: "dVs (set E_impl) = set (map prod.fst E_impl) ∪ set (map prod.snd E_impl)"
  by(induction E_impl) auto

lemma dVs_swap: "dVs (prod.swap ` E) = dVs E"
  by(auto simp add: dVs_def)

end