Theory FiniteListGraph

theory FiniteListGraph
imports 
  FiniteGraph
  "Transitive-Closure.Transitive_Closure_List_Impl"
begin

section ‹Specification of a finite graph, implemented by lists›

text‹A graph ‹G=(V,E)› consits of a list of vertices @{term V}, also called nodes, 
       and a list of edges @{term E}. The edges are tuples of vertices.
       Using lists instead of sets, code can be easily created.›

  record 'v list_graph =
    nodesL :: "'v list"
    edgesL :: "('v ×'v) list"

text‹Correspondence the FiniteGraph›
  definition list_graph_to_graph :: "'v list_graph ⇒ 'v graph" where 
    "list_graph_to_graph G = ⦇ nodes = set (nodesL G), edges = set (edgesL G) ⦈"


  definition wf_list_graph_axioms :: "'v list_graph ⇒ bool" where
    "wf_list_graph_axioms G ⟷ fst` set (edgesL G) ⊆ set (nodesL G) ∧ snd` set (edgesL G) ⊆ set (nodesL G)"


  lemma wf_list_graph_iff_wf_graph: "wf_graph (list_graph_to_graph G) ⟷ wf_list_graph_axioms G"
  unfolding list_graph_to_graph_def wf_graph_def wf_list_graph_axioms_def
  by simp

  text‹We say a @{typ "'v list_graph"} is valid if it fulfills the graph axioms and its lists are distinct›
  definition wf_list_graph::"('v) list_graph ⇒ bool" where
   "wf_list_graph G = (distinct (nodesL G) ∧ distinct (edgesL G) ∧ wf_list_graph_axioms G)"


section‹FiniteListGraph operations›

  text ‹Adds a node to a graph.›
  definition add_node :: "'v ⇒ 'v list_graph ⇒ 'v list_graph" where 
    "add_node v G = ⦇ nodesL = (if v ∈ set (nodesL G) then nodesL G else v#nodesL G), edgesL=edgesL G ⦈"

  text ‹Adds an edge to a graph.›
  definition add_edge :: "'v ⇒ 'v ⇒ 'v list_graph ⇒ 'v list_graph" where 
    "add_edge v v' G = (add_node v (add_node v' G)) ⦇edgesL := (if (v, v') ∈ set (edgesL G) then edgesL G else (v, v')#edgesL G) ⦈"

  text ‹Deletes a node from a graph. Also deletes all adjacent edges.›
  definition delete_node :: "'v ⇒ 'v list_graph ⇒ 'v list_graph" where 
  "delete_node v G = ⦇ 
    nodesL = remove1 v (nodesL G), edgesL = [(e1,e2) ← (edgesL G). e1 ≠ v ∧ e2 ≠ v]
    ⦈"

  text ‹Deletes an edge from a graph.›
  definition delete_edge :: "'v ⇒ 'v ⇒ 'v list_graph ⇒ 'v list_graph" where 
    "delete_edge v v' G = ⦇nodesL = nodesL G, edgesL = [(e1,e2) ← edgesL G. e1 ≠ v ∨ e2 ≠ v'] ⦈"

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



text ‹extended graph operations›
   text ‹Reflexive transitive successors of a node. Or: All reachable nodes for v including v.›
    definition succ_rtran :: "'v list_graph ⇒ 'v ⇒ 'v list" where
      "succ_rtran G v = rtrancl_list_impl (edgesL G) [v]"

   text ‹Transitive successors of a node. Or: All reachable nodes for v.›
    definition succ_tran :: "'v list_graph ⇒ 'v ⇒ 'v list" where
      "succ_tran G v = trancl_list_impl (edgesL G) [v]"
  
   text ‹The number of reachable nodes from v›
    definition num_reachable :: "'v list_graph ⇒ 'v ⇒ nat" where
      "num_reachable G v = length (succ_tran G v)"


    definition num_reachable_norefl :: "'v list_graph ⇒ 'v ⇒ nat" where
      "num_reachable_norefl G v = length ([ x ← succ_tran G v. x ≠ v])"


subsection‹undirected graph simulation›
  text ‹Create undirected graph from directed graph by adding backward links›
  fun backlinks :: "('v × 'v) list ⇒ ('v × 'v) list" where
    "backlinks [] = []" |
    "backlinks ((e1, e2)#es) = (e2, e1)#(backlinks es)"

  definition undirected :: "'v list_graph ⇒ 'v list_graph"
    where "undirected G ≡ ⦇ nodesL = nodesL G, edgesL = remdups (edgesL G @ backlinks (edgesL G)) ⦈"

section‹Correctness lemmata›

  ― ‹add node›
  lemma add_node_wf: "wf_list_graph G ⟹ wf_list_graph (add_node v G)"
  unfolding wf_list_graph_def wf_list_graph_axioms_def add_node_def
  by auto

  lemma add_node_set_nodes: "set (nodesL (add_node v G)) = set (nodesL G) ∪ {v}"
  unfolding add_node_def
  by auto

  lemma add_node_set_edges: "set (edgesL (add_node v G)) = set (edgesL G)"
  unfolding add_node_def
  by auto

  lemma add_node_correct: "FiniteGraph.add_node v (list_graph_to_graph G) = list_graph_to_graph (add_node v G)"
  unfolding FiniteGraph.add_node_def list_graph_to_graph_def
  by (simp add: add_node_set_edges add_node_set_nodes)

  lemma add_node_wf2: "wf_graph (list_graph_to_graph G) ⟹ wf_graph (list_graph_to_graph (add_node v G))"
  by (subst add_node_correct[symmetric]) simp

  ― ‹add edge›
  lemma add_edge_wf: "wf_list_graph G ⟹ wf_list_graph (add_edge v v' G)"
  unfolding wf_list_graph_def add_edge_def add_node_def wf_list_graph_axioms_def
  by auto

  lemma add_edge_set_nodes: "set (nodesL (add_edge v v' G)) = set (nodesL G) ∪ {v,v'}"
  unfolding add_edge_def add_node_def
  by auto

  lemma add_edge_set_edges: "set (edgesL (add_edge v v' G)) = set (edgesL G) ∪ {(v,v')}"
  unfolding add_edge_def add_node_def
  by auto

  lemma add_edge_correct: "FiniteGraph.add_edge v v' (list_graph_to_graph G) = list_graph_to_graph (add_edge v v' G)"
  unfolding FiniteGraph.add_edge_def add_edge_def list_graph_to_graph_def
  by (auto simp: add_node_set_nodes)

  lemma add_edge_wf2: "wf_graph (list_graph_to_graph G) ⟹ wf_graph (list_graph_to_graph (add_edge v v' G))"
  by (subst add_edge_correct[symmetric]) simp

  ― ‹delete node›
  lemma delete_node_wf: "wf_list_graph G ⟹ wf_list_graph (delete_node v G)"
  unfolding wf_list_graph_def delete_node_def wf_list_graph_axioms_def
  by auto

  lemma delete_node_set_edges:
    "set (edgesL (delete_node v G)) = {(a,b). (a, b) ∈ set (edgesL G) ∧ a ≠ v ∧ b ≠ v}"
  unfolding delete_node_def
  by auto

  lemma delete_node_correct:
    assumes "wf_list_graph G"
    shows "FiniteGraph.delete_node v (list_graph_to_graph G) = list_graph_to_graph (delete_node v G)"
  using assms
  unfolding FiniteGraph.delete_node_def delete_node_def list_graph_to_graph_def wf_list_graph_def
  by auto

  ― ‹delete edge›
  lemma delete_edge_set_nodes: "set (nodesL (delete_edge v v' G)) = set (nodesL G)"
  unfolding delete_edge_def
  by simp

  lemma delete_edge_set_edges:
    "set (edgesL (delete_edge v v' G)) = {(a,b). (a,b) ∈ set (edgesL G) ∧ (a,b) ≠ (v,v')}"
  unfolding delete_edge_def
  by auto

  lemma delete_edge_set_edges2:
    "set (edgesL (delete_edge v v' G)) = set (edgesL G) - {(v,v')}"
  by (auto simp:delete_edge_set_edges)

  lemma delete_edge_wf: "wf_list_graph G ⟹ wf_list_graph (delete_edge v v' G)"
  unfolding wf_list_graph_def delete_edge_def wf_list_graph_axioms_def
  by auto
    
  lemma delete_edge_length: "length (edgesL (delete_edge v v' G)) ≤ length (edgesL G)"
  unfolding delete_edge_def
  by simp

  lemma delete_edge_commute: "delete_edge a1 a2 (delete_edge b1 b2 G) = delete_edge b1 b2 (delete_edge a1 a2 G)"
  unfolding delete_edge_def
  by simp metis (* auto doesn't seem to like filter_cong *)

  lemma delete_edge_correct: "FiniteGraph.delete_edge v v' (list_graph_to_graph G) = list_graph_to_graph (delete_edge v v' G)"
  unfolding FiniteGraph.delete_edge_def delete_edge_def list_graph_to_graph_def
  by auto

  lemma delete_edge_wf2: "wf_graph (list_graph_to_graph G) ⟹ wf_graph (list_graph_to_graph (delete_edge v v' G))"
  by (subst delete_edge_correct[symmetric]) simp

  ― ‹delete edges›
  lemma delete_edges_wf: "wf_list_graph G ⟹ wf_list_graph (delete_edges G E)"
  by (induction E arbitrary: G) (auto simp: delete_edge_wf)

  lemma delete_edges_set_nodes: "set (nodesL (delete_edges G E)) = set (nodesL G)"
  by (induction E arbitrary: G) (auto simp: delete_edge_set_nodes)

  lemma delete_edges_nodes: "nodesL (delete_edges G es) = nodesL G"
  by (induction es arbitrary: G) (auto simp: delete_edge_def)

  lemma delete_edges_set_edges: "set (edgesL (delete_edges G E)) = set (edgesL G) - set E"
  by (induction E arbitrary: G) (auto simp: delete_edge_def delete_edge_set_nodes)

  lemma delete_edges_set_edges2:
    "set (edgesL (delete_edges G E)) = {(a,b). (a,b) ∈ set (edgesL G) ∧ (a,b) ∉ set E}"
  by (auto simp: delete_edges_set_edges)

  lemma delete_edges_length: "length (edgesL (delete_edges G f)) ≤ length (edgesL G)"
  proof (induction f arbitrary:G)
    case (Cons f fs)
    thus ?case
      apply (cases f, hypsubst)
      apply (subst delete_edges.simps(2))
      apply (metis delete_edge_length le_trans)
      done
  qed simp

  lemma delete_edges_chain: "delete_edges G (as @ bs) = delete_edges (delete_edges G as) bs"
  proof (induction as arbitrary: bs G)
    case (Cons f fs)
    thus ?case
      by (cases f) auto
  qed simp

  lemma delete_edges_delete_edge_commute:
    "delete_edges (delete_edge a1 a2 G) as = delete_edge a1 a2 (delete_edges G as)"
  proof (induction as arbitrary: G a1 a2)
    case (Cons f fs)
    thus ?case
      by (cases f) (simp add: delete_edge_commute)
  qed simp

  lemma delete_edges_commute:
    "delete_edges (delete_edges G as) bs = delete_edges (delete_edges G bs) as"
  proof (induction as arbitrary: bs G)
    case (Cons f fs)
    thus ?case
      by (cases f) (simp add: delete_edges_delete_edge_commute)
  qed simp

  lemma delete_edges_as_filter:
    "delete_edges G l = ⦇ nodesL = nodesL G,  edgesL = [x ← edgesL G. x ∉ set l] ⦈"
  proof (induction l)
    case (Cons f fs)
    thus ?case
      apply (cases f)
      apply (simp add: delete_edges_delete_edge_commute)
      apply (simp add: delete_edge_def)
      apply (metis (lifting, full_types) prod.exhaust case_prodI split_conv)
      done
  qed simp

  declare delete_edges.simps[simp del] (*do not automatically expand definition*)

  lemma delete_edges_correct:
    "FiniteGraph.delete_edges (list_graph_to_graph G) (set E) = list_graph_to_graph (delete_edges G E)"
  unfolding list_graph_to_graph_def FiniteGraph.delete_edges_def
  by (auto simp add: delete_edges_as_filter )
  
  lemma delete_edges_wf2:
    "wf_graph (list_graph_to_graph G) ⟹ wf_graph (list_graph_to_graph (delete_edges G E))"
  by (subst delete_edges_correct[symmetric]) simp

  ― ‹helper about reflexive transitive closure impl›
  lemma distinct_relpow_impl:
    "distinct L ⟹ distinct new ⟹ distinct have ⟹ distinct (new@have) ⟹ 
     distinct (relpow_impl (λas. remdups (map snd [(a, b)←L . a ∈ set as])) (λxs ys. [x←xs . x ∉ set ys] @ ys) (λx xs. x ∈ set xs) new have M)"
  proof (induction M arbitrary: "new" "have")
    case Suc
    hence
      "distinct ([x←new . x ∉ set have] @ have)"
      "set ([n←remdups (map snd [(a, b)←L . a ∈ set new]) . (n ∈ set new ⟶ n ∈ set have) ∧ n ∉ set have]) ∩ set ([x←new . x ∉ set have] @ have) = {}"
      by auto

    with Suc show ?case
      by auto
  qed auto

  lemma distinct_rtrancl_list_impl: "distinct L ⟹ distinct ls ⟹ distinct (rtrancl_list_impl L ls)"
  unfolding rtrancl_list_impl_def rtrancl_impl_def
  by (simp add:distinct_relpow_impl)

  lemma distinct_trancl_list_impl: "distinct L ⟹ distinct ls ⟹ distinct (trancl_list_impl L ls)"
  unfolding trancl_list_impl_def trancl_impl_def
  by (simp add:distinct_relpow_impl)

  ― ‹succ rtran›
  value "succ_rtran ⦇ nodesL = [1::nat,2,3,4,8,9,10], edgesL = [(1,2), (2,3), (3,4), (8,9),(9,8)] ⦈ 1"

  lemma succ_rtran_correct: "FiniteGraph.succ_rtran (list_graph_to_graph G) v = set (succ_rtran G v)"
  unfolding FiniteGraph.succ_rtran_def succ_rtran_def list_graph_to_graph_def
  by (simp add: rtrancl_list_impl)

  lemma distinct_succ_rtran: "wf_list_graph G ⟹ distinct (succ_rtran G v)"
  unfolding succ_rtran_def wf_list_graph_def
  by (auto intro: distinct_rtrancl_list_impl)

  lemma succ_rtran_set: "set (succ_rtran G v) = {e2. (v,e2) ∈ (set (edgesL G))⇧*}"
  unfolding succ_rtran_def
  by (simp add: rtrancl_list_impl)

  ― ‹succ tran›
  lemma distinct_succ_tran: "wf_list_graph G ⟹ distinct (succ_tran G v)"
  unfolding succ_tran_def wf_list_graph_def
  by (auto intro: distinct_trancl_list_impl)

  lemma succ_tran_set: "set (succ_tran G v) = {e2. (v,e2) ∈ (set (edgesL G))⇧+}"
  unfolding succ_tran_def
  by (simp add: trancl_list_impl)

  value "succ_tran ⦇ nodesL = [1::nat,2,3,4,8,9,10], edgesL = [(1,2), (2,3), (3,4), (8,9),(9,8)] ⦈ 1"

  lemma succ_tran_correct: "FiniteGraph.succ_tran (list_graph_to_graph G) v = set (succ_tran G v)"
  unfolding FiniteGraph.succ_tran_def succ_tran_def list_graph_to_graph_def
  by (simp add:trancl_list_impl)
  
  ― ‹num_reachable›
  lemma num_reachable_correct:
    "wf_list_graph G ⟹ FiniteGraph.num_reachable (list_graph_to_graph G) v = num_reachable G v"
  unfolding num_reachable_def FiniteGraph.num_reachable_def
  by (metis List.distinct_card distinct_succ_tran succ_tran_correct)

  ― ‹num_reachable_norefl›
  lemma num_reachable_norefl_correct:
    "wf_list_graph G ⟹ 
     FiniteGraph.num_reachable_norefl (list_graph_to_graph G) v = num_reachable_norefl G v"
 unfolding num_reachable_norefl_def FiniteGraph.num_reachable_norefl_def
 by (metis (full_types) List.distinct_card distinct_filter distinct_succ_tran set_minus_filter_out succ_tran_correct)

  ― ‹backlinks, i.e. backflows in formal def›
  lemma backlinks_alt: "backlinks E = [(snd e, fst e). e ← E]"
  by (induction E) auto

  lemma backlinks_set: "set (backlinks E) = {(e2, e1). (e1, e2) ∈ set E}"
  by (induction E) auto

  lemma undirected_nodes_set: "set (edgesL (undirected G)) = set (edgesL G) ∪ {(e2, e1). (e1, e2) ∈ set (edgesL G)}"
  unfolding undirected_def
  by (simp add: backlinks_set)

  lemma undirected_succ_tran_set: "set (succ_tran (undirected G) v) = {e2. (v,e2) ∈ (set (edgesL (undirected G)))⇧+}"
  by (fact succ_tran_set)

  lemma backlinks_in_nodes_G: "⟦ fst ` set (edgesL G) ⊆ set (nodesL G); snd ` set (edgesL G) ⊆ set (nodesL G) ⟧ ⟹ 
    fst` set (edgesL (undirected G)) ⊆ set (nodesL (undirected G)) ∧ snd` set (edgesL (undirected G)) ⊆ set (nodesL (undirected G))"
  unfolding undirected_def
  by(auto simp: backlinks_set)

  lemma backlinks_distinct: "distinct E ⟹ distinct (backlinks E)"
  by (induction E) (auto simp: backlinks_alt)

  lemma backlinks_subset: "set (backlinks X) ⊆ set (backlinks Y) ⟷ set X ⊆ set Y"
  by (auto simp: backlinks_set)

  lemma backlinks_correct: "FiniteGraph.backflows (set E) = set (backlinks E)"
  unfolding backflows_def
  by(simp add: backlinks_set)

  ― ‹undirected›
  lemma undirected_wf: "wf_list_graph G ⟹ wf_list_graph (undirected G)"
  unfolding wf_list_graph_def wf_list_graph_axioms_def
  by (simp add:backlinks_in_nodes_G) (simp add: undirected_def)

  lemma undirected_correct: 
    "FiniteGraph.undirected (list_graph_to_graph G) = list_graph_to_graph (undirected G)"
  unfolding FiniteGraph.undirected_def undirected_def list_graph_to_graph_def
  by (simp add: backlinks_set)
      
lemmas wf_list_graph_wf =
  add_node_wf
  add_edge_wf
  delete_node_wf
  delete_edge_wf
  delete_edges_wf
  undirected_wf

lemmas list_graph_correct =
  add_node_correct
  add_edge_correct
  delete_node_correct
  delete_edge_correct
  delete_edges_correct
  succ_rtran_correct
  succ_tran_correct
  num_reachable_correct
  undirected_correct


end