Theory FiniteGraph

theory FiniteGraph
imports Main 
begin

(*Lots of this theory is based on a work by Benedikt Nordhoff and Peter Lammich*)

section ‹Specification of a finite directed graph›

text‹A graph ‹G=(V,E)› consits of a set of vertices ‹V›, also called nodes, 
       and a set of edges ‹E›. The edges are tuples of vertices. Both, 
       the set of vertices and edges is finite.›

(* Inspired by
Title: Dijkstra's Shortest Path Algorithm
Author: Benedikt Nordhoff and Peter Lammich
http://isa-afp.org/entries/Dijkstra_Shortest_Path.shtml
*)

section ‹Graph›
subsection‹Definitions›
  text ‹A graph is represented by a record.›
  record 'v graph =
    nodes :: "'v set"
    edges :: "('v ×'v) set"

  text ‹In a well-formed graph, edges only go from nodes to nodes.›
  locale wf_graph = 
    fixes G :: "'v graph"
    ― ‹Edges only reference to existing nodes›
    assumes E_wf: "fst ` (edges G) ⊆ (nodes G)"
                     "snd ` (edges G) ⊆ (nodes G)"
    and finiteE: "finite (edges G)" (*implied by finiteV*)
    and finiteV: "finite (nodes G)"
  begin
    abbreviation "V ≡ (nodes G)"
    abbreviation "E ≡ (edges G)"

    lemma E_wfD: assumes "(v,v') ∈ E"
      shows "v ∈ V" "v' ∈ V"
      apply -
       apply (rule subsetD[OF E_wf(1)])
       using assms apply force
      apply (rule subsetD[OF E_wf(2)])
      using assms apply force
      done

    lemma E_wfD2: "∀e ∈ E. fst e ∈ V ∧ snd e ∈ V"
    by (auto simp add: E_wfD)
  end

subsection ‹Basic operations on Graphs›
  text ‹The empty graph.›
  definition empty :: "'v graph" where 
    "empty ≡ ⦇ nodes = {}, edges = {} ⦈"

  text ‹Adds a node to a graph.›
  definition add_node :: "'v ⇒ 'v graph ⇒ 'v graph" where 
    "add_node v G ≡ ⦇ nodes = ({v} ∪ (nodes G)), edges=edges G ⦈"

  text ‹Deletes a node from a graph. Also deletes all adjacent edges.›
  definition delete_node where "delete_node v G ≡ ⦇ 
      nodes = (nodes G) - {v},   
      edges = {(e1, e2). (e1, e2) ∈ edges G ∧ e1 ≠ v ∧ e2 ≠ v}
    ⦈"

  text ‹Adds an edge to a graph.›
  definition add_edge where 
  "add_edge v v' G = ⦇nodes = nodes G ∪ {v,v'}, edges = {(v, v')} ∪ edges G ⦈"

  text ‹Deletes an edge from a graph.›
  definition delete_edge where "delete_edge v v' G ≡ ⦇
      nodes = nodes G, 
      edges = {(e1,e2). (e1, e2) ∈ edges G ∧ (e1,e2) ≠ (v,v')}
    ⦈"
  
  definition delete_edges::"'v graph ⇒ ('v × 'v) set ⇒ 'v graph" where 
    "delete_edges G es ≡ ⦇
      nodes = nodes G, 
      edges = {(e1,e2). (e1, e2) ∈ edges G ∧ (e1,e2) ∉ es}
    ⦈"

  fun delete_edges_list::"'v graph ⇒ ('v × 'v) list ⇒ 'v graph" where 
    "delete_edges_list G [] = G"|
    "delete_edges_list G ((v,v')#es) = delete_edges_list (delete_edge v v' G) es"

  definition fully_connected :: "'v graph ⇒ 'v graph" where
    "fully_connected G ≡ ⦇nodes = nodes G, edges = nodes G × nodes G ⦈"


text ‹Extended graph operations›
  text ‹Reflexive transitive successors of a node. Or: All reachable nodes for ‹v› including ‹v›.›
  definition succ_rtran :: "'v graph ⇒ 'v ⇒ 'v set" where
    "succ_rtran G v = {e2. (v,e2) ∈ (edges G)⇧*}"

  text ‹Transitive successors of a node. Or: All reachable nodes for ‹v›.›
  definition succ_tran :: "'v graph ⇒ 'v ⇒ 'v set" where
    "succ_tran G v = {e2. (v,e2) ∈ (edges G)⇧+}"

  ― ‹succ_tran is always finite›
  lemma succ_tran_finite: "wf_graph G ⟹ finite (succ_tran G v)"
  proof -
    assume "wf_graph G"
    from wf_graph.finiteE[OF this] have "finite ((edges G)⇧+)" using finite_trancl[symmetric, of "edges G"] by metis
    from this have "finite {(e1,e2). (e1, e2) ∈ (edges G)⇧+}" by simp
    from this have finite: "finite (snd ` {(e1,e2). (e1, e2) ∈ (edges G)⇧+})" by (metis finite_imageI)
    have "{(e1,e2). (e1, e2) ∈ (edges G)⇧+ ∧ e1 = v} ⊆ {(e1,e2). (e1, e2) ∈ (edges G)⇧+}" by blast
    have 1: "snd ` {(e1,e2). (e1, e2) ∈ (edges G)⇧+ ∧ e1 = v} ⊆ snd ` {(e1,e2). (e1, e2) ∈ (edges G)⇧+}" by blast
    have 2: "snd ` {(e1,e2). (e1, e2) ∈ (edges G)⇧+ ∧ e1 = v} = {e2. (v,e2) ∈ (edges G)⇧+}" by force
    from 1 2 have "{e2. (v,e2) ∈ (edges G)⇧+} ⊆ snd ` {(e1,e2). (e1, e2) ∈ (edges G)⇧+}" by blast
    from this finite have "finite {e2. (v, e2) ∈ (edges G)⇧+}" by (metis finite_subset)
    thus "finite (succ_tran G v)" using succ_tran_def by metis
  qed
  
  text‹If there is no edge leaving from ‹v›, then ‹v› has no successors›
  lemma succ_tran_empty: "⟦ wf_graph G; v ∉ (fst ` edges G) ⟧ ⟹ succ_tran G v = {}"
    unfolding succ_tran_def using image_iff tranclD by fastforce

  text‹@{const succ_tran} is subset of nodes›
  lemma succ_tran_subseteq_nodes: "⟦ wf_graph G ⟧ ⟹ succ_tran G v ⊆ nodes G"
    unfolding succ_tran_def using tranclD2 wf_graph.E_wfD(2) by fastforce

  text ‹The number of reachable nodes from ‹v››
  definition num_reachable :: "'v graph ⇒ 'v ⇒ nat" where
    "num_reachable G v = card (succ_tran G v)"

  definition num_reachable_norefl :: "'v graph ⇒ 'v ⇒ nat" where
    "num_reachable_norefl G v = card (succ_tran G v - {v})"

  text‹@{const card} returns @{term 0} for infinite sets.
        Here, for a well-formed graph, if @{const num_reachable} is zero, there are actually no nodes reachable.›
  lemma num_reachable_zero: "⟦wf_graph G; num_reachable G v = 0⟧ ⟹ succ_tran G v = {}"
  unfolding num_reachable_def
  apply(subgoal_tac "finite (succ_tran G v)")
   apply(simp)
  apply(blast intro: succ_tran_finite)
  done
  lemma num_succtran_zero: "⟦succ_tran G v = {}⟧ ⟹ num_reachable G v = 0"
    unfolding num_reachable_def by simp
  lemma num_reachable_zero_iff: "⟦wf_graph G⟧ ⟹ (num_reachable G v = 0) ⟷ (succ_tran G v = {})"
  by(metis num_succtran_zero num_reachable_zero)


section‹Undirected Graph›

subsection‹undirected graph simulation›
  text ‹Create undirected graph from directed graph by adding backward links›

  definition backflows :: "('v × 'v) set ⇒ ('v × 'v) set" where
    "backflows E ≡ {(r,s). (s,r) ∈ E}"

  definition undirected :: "'v graph ⇒ 'v graph"
    where "undirected G = ⦇ nodes = nodes G, edges = (edges G) ∪ {(b,a). (a,b) ∈ edges G} ⦈"

section ‹Graph Lemmas›

  lemma graph_eq_intro: "(nodes (G::'a graph) = nodes G') ⟹ (edges G = edges G') ⟹ G = G'" by simp

  ― ‹finite›
  lemma wf_graph_finite_filterE: "wf_graph G ⟹ finite {(e1, e2). (e1, e2) ∈ edges G ∧ P e1 e2}"
  by(simp add: wf_graph.finiteE split_def)
  lemma wf_graph_finite_filterV: "wf_graph G ⟹ finite {n. n ∈ nodes G ∧ P n}"
  by(simp add: wf_graph.finiteV)

  ― ‹empty›
  lemma empty_wf[simp]: "wf_graph empty"
    unfolding empty_def by unfold_locales auto
  lemma nodes_empty[simp]: "nodes empty = {}" unfolding empty_def by simp
  lemma edges_empty[simp]: "edges empty = {}" unfolding empty_def by simp

  ― ‹add node›
  lemma add_node_wf[simp]: "wf_graph g ⟹ wf_graph (add_node v g)"
    unfolding add_node_def wf_graph_def by (auto)

  lemma delete_node_wf[simp]: "wf_graph G ⟹ wf_graph (delete_node v G)"
    by(auto simp add: delete_node_def wf_graph_def wf_graph_finite_filterE)

  ― ‹add edgde›
  lemma add_edge_wf[simp]: "wf_graph G ⟹ wf_graph (add_edge v v' G)"
    by(auto simp add: add_edge_def add_node_def wf_graph_def)

  ― ‹delete edge›
  lemma delete_edge_wf[simp]: "wf_graph G ⟹ wf_graph (delete_edge v v' G)"
    by(auto simp add: delete_edge_def add_node_def wf_graph_def split_def)
 
  ― ‹delte edges›
  lemma delete_edges_list_wf[simp]: "wf_graph G ⟹ wf_graph (delete_edges_list G E)"
    by(induction E arbitrary: G, simp, force)
  lemma delete_edges_wf[simp]: "wf_graph G ⟹ wf_graph (delete_edges G E)"
    by(auto simp add: delete_edges_def add_node_def wf_graph_def split_def)
  lemma delete_edges_list_set: "delete_edges_list G E = delete_edges G (set E)"
    proof(induction E arbitrary: G)
    case Nil thus ?case by (simp add: delete_edges_def)
    next
    case (Cons e E) thus ?case by(cases e)(simp add: delete_edge_def delete_edges_def)
    qed
  lemma delete_edges_list_union: "delete_edges_list G (ff @ keeps) = delete_edges G (set ff ∪ set keeps)"
   by(simp add: delete_edges_list_set)
  lemma add_edge_delete_edges_list: 
    "(add_edge (fst a) (snd a) (delete_edges_list G (a # ff))) = (add_edge (fst a) (snd a) (delete_edges G (set ff)))"
   by(auto simp add: delete_edges_list_set delete_edges_def add_edge_def add_node_def)
  lemma delete_edges_empty[simp]: "delete_edges G {} = G"
   by(simp add: delete_edges_def)
  lemma delete_edges_simp2: "delete_edges G E = ⦇ nodes = nodes G, edges = edges G - E⦈"
   by(auto simp add: delete_edges_def)
  lemma delete_edges_set_nodes: "nodes (delete_edges G E) = nodes G"
   by(simp add: delete_edges_simp2)
  lemma delete_edges_edges_mono: "E' ⊆ E ⟹ edges (delete_edges G E) ⊆ edges (delete_edges G E')"
    by(simp add: delete_edges_def, fast)
  lemma delete_edges_edges_empty: "(delete_edges G (edges G)) = G⦇edges := {}⦈"
    by(simp add: delete_edges_simp2)

 ― ‹add delete›
  lemma add_delete_edge: "wf_graph (G::'a graph) ⟹ (a,b) ∈ edges G ⟹ add_edge a b (delete_edge a b G) = G"
   apply(simp add: delete_edge_def add_edge_def wf_graph_def)
   apply(intro graph_eq_intro)
    by auto

  lemma add_delete_edges: "wf_graph (G::'v graph) ⟹ (a,b) ∈ edges G ⟹ (a,b) ∉ fs ⟹
    add_edge a b (delete_edges G (insert (a, b) fs)) = (delete_edges G fs)"
    by(auto simp add: delete_edges_simp2 add_edge_def wf_graph_def)


 ― ‹fully_connected›
  lemma fully_connected_simp: "fully_connected ⦇nodes = N, edges = ignore ⦈≡ ⦇nodes = N, edges = N × N ⦈"
    by(simp add: fully_connected_def)
  lemma fully_connected_wf: "wf_graph G ⟹ wf_graph (fully_connected G)"
    by(simp add: fully_connected_def wf_graph_def)

 ― ‹succ_tran›
 lemma succ_tran_mono: 
  "wf_graph ⦇nodes=N, edges=E⦈ ⟹ E' ⊆ E ⟹ succ_tran ⦇nodes=N, edges=E'⦈ v ⊆ succ_tran ⦇nodes=N, edges=E⦈ v"
   apply(drule wf_graph.finiteE)
   apply(frule_tac A="E'" in rev_finite_subset, simp)
   apply(simp add: num_reachable_def)
   apply(simp add: succ_tran_def)
   apply(metis (lifting, full_types) Collect_mono trancl_mono)
  done

  ― ‹num_reachable›
  lemma num_reachable_mono:
  "wf_graph ⦇nodes=N, edges=E⦈ ⟹ E' ⊆ E ⟹ num_reachable ⦇nodes=N, edges=E'⦈ v ≤ num_reachable ⦇nodes=N, edges=E⦈ v"
   apply(simp add: num_reachable_def)
   apply(frule_tac E'="E'" and v="v" in succ_tran_mono, simp)
   apply(frule_tac v="v" in succ_tran_finite)
   apply(simp add: card_mono)
  done

  ― ‹num_reachable_norefl›
  lemma num_reachable_norefl_mono:
  "wf_graph ⦇nodes=N, edges=E⦈ ⟹ E' ⊆ E ⟹ num_reachable_norefl ⦇nodes=N, edges=E'⦈ v ≤ num_reachable_norefl ⦇nodes=N, edges=E⦈ v"
   apply(simp add: num_reachable_norefl_def)
   apply(frule_tac E'="E'" and v="v" in succ_tran_mono, simp)
   apply(frule_tac v="v" in succ_tran_finite)
   using card_mono by (metis Diff_mono finite_Diff subset_refl)

  ― ‹backflows›
  lemma backflows_wf: 
    "wf_graph ⦇nodes=N, edges=E⦈ ⟹ wf_graph ⦇nodes=N, edges=backflows E⦈"
    using [[simproc add: finite_Collect]] by(auto simp add: wf_graph_def backflows_def)
  lemma undirected_backflows: 
    "undirected G = ⦇ nodes = nodes G, edges = (edges G) ∪ backflows (edges G) ⦈"
    by(simp add: backflows_def undirected_def)
  lemma backflows_id: 
    "backflows (backflows E) = E"
    by(simp add: backflows_def)
  lemma backflows_finite: "finite E ⟹ finite (backflows E)"
    using [[simproc add: finite_Collect]] by(simp add: backflows_def) 
  lemma backflows_minus_backflows: "backflows (X - backflows Y) = (backflows X) - Y"
    by(auto simp add: backflows_def)
  lemma backflows_subseteq: "X ⊆ Y ⟷ backflows X ⊆ backflows Y"
    by(auto simp add: backflows_def)
  lemma backflows_un: "backflows (A ∪ B) = (backflows A) ∪ (backflows B)"
    by(auto simp add: backflows_def)
  lemma backflows_inter: "backflows (A ∩ B) = (backflows A) ∩ (backflows B)"
    by(auto simp add: backflows_def)
  lemma backflows_alt_fstsnd: "backflows E = (λe. (snd e, fst e)) ` E"
    by(auto simp add: backflows_def, force)


lemmas graph_ops=add_node_def delete_node_def add_edge_def delete_edge_def delete_edges_simp2


  ― ‹wf_graph›
  lemma wf_graph_remove_edges: "wf_graph ⦇ nodes = V, edges = E ⦈ ⟹ wf_graph ⦇ nodes = V, edges=E - X⦈"
    by (metis delete_edges_simp2 delete_edges_wf select_convs(1) select_convs(2))

  lemma wf_graph_remove_edges_union: 
    "wf_graph ⦇ nodes = V, edges = E ∪ E' ⦈ ⟹ wf_graph ⦇ nodes = V, edges=E⦈"
    by(auto simp add: wf_graph_def)

  lemma wf_graph_union_edges: "⟦ wf_graph ⦇ nodes = V, edges = E ⦈; wf_graph ⦇ nodes = V, edges=E'⦈ ⟧ ⟹
     wf_graph ⦇ nodes = V, edges=E ∪ E'⦈"
    by(auto simp add: wf_graph_def)

  lemma wf_graph_add_subset_edges: "⟦ wf_graph ⦇ nodes = V, edges = E ⦈; E' ⊆ E ⟧ ⟹
     wf_graph ⦇ nodes = V, edges= E ∪ E'⦈"
    by(auto simp add: wf_graph_def) (metis rev_finite_subset)


(*Inspired by 
Benedikt Nordhoff and Peter Lammich
Dijkstra's Shortest Path Algorithm
http://isa-afp.org/entries/Dijkstra_Shortest_Path.shtml*)
(*more a literal copy of http://isa-afp.org/browser_info/current/AFP/Dijkstra_Shortest_Path/Graph.html*)

  text ‹Successors of a node.›
  definition succ :: "'v graph ⇒ 'v ⇒ 'v set"
    where "succ G v ≡ {v'. (v,v')∈edges G}"


  lemma succ_finite[simp, intro]: "finite (edges G) ⟹ finite (succ G v)"
    unfolding succ_def
    by (rule finite_subset[where B="snd`edges G"]) force+

  lemma succ_empty: "succ empty v = {}" unfolding empty_def succ_def by auto

  lemma (in wf_graph) succ_subset: "succ G v ⊆ V"
    unfolding succ_def using E_wf
    by (force)


end