Theory Dijkstra_Shortest_Path.GraphSpec

section "Graph Interface"
theory GraphSpec
imports Main Graph 
  Collections.Collections 
  (*"../Collections/Lib/Proper_Iterator"*)
  (*"../Refine_Monadic/Refine_Autodet"*)
begin
  text ‹
    This theory defines an ICF-style interface for graphs.
›

  type_synonym ('V,'W,'G) graph_α = "'G ⇒ ('V,'W) graph"

  locale graph =
    fixes α :: "'G ⇒ ('V,'W) graph"
    fixes invar :: "'G ⇒ bool"
    assumes finite[simp, intro!]:
      "invar g ⟹ finite (nodes (α g))"
      "invar g ⟹ finite (edges (α g))"
    assumes valid: "invar g ⟹ valid_graph (α g)"

  type_synonym ('V,'W,'G) graph_empty = "unit ⇒ 'G"
  locale graph_empty = graph +
    constrains α :: "'G ⇒ ('V,'W) graph"
    fixes empty :: "unit ⇒ 'G"
    assumes empty_correct:
      "α (empty ()) = Graph.empty"
      "invar (empty ())"

  type_synonym ('V,'W,'G) graph_add_node = "'V ⇒ 'G ⇒ 'G"
  locale graph_add_node = graph +
    constrains α :: "'G ⇒ ('V,'W) graph"
    fixes add_node :: "'V ⇒ 'G ⇒ 'G"
    assumes add_node_correct:
      "invar g ⟹ invar (add_node v g)"
      "invar g ⟹ α (add_node v g) = Graph.add_node v (α g)"

  type_synonym ('V,'W,'G) graph_delete_node = "'V ⇒ 'G ⇒ 'G"
  locale graph_delete_node = graph +
    constrains α :: "'G ⇒ ('V,'W) graph"
    fixes delete_node :: "'V ⇒ 'G ⇒ 'G"
    assumes delete_node_correct:
      "invar g ⟹ invar (delete_node v g)"
      "invar g ⟹ α (delete_node v g) = Graph.delete_node v (α g)"

  type_synonym ('V,'W,'G) graph_add_edge = "'V ⇒'W ⇒ 'V ⇒ 'G ⇒ 'G"
  locale graph_add_edge = graph +
    constrains α :: "'G ⇒ ('V,'W) graph"
    fixes add_edge :: "'V ⇒ 'W ⇒ 'V ⇒ 'G ⇒ 'G"
    assumes add_edge_correct:
      "invar g ⟹ invar (add_edge v e v' g)"
      "invar g ⟹ α (add_edge v e v' g) = Graph.add_edge v e v' (α g)"

  type_synonym ('V,'W,'G) graph_delete_edge = "'V ⇒'W ⇒ 'V ⇒ 'G ⇒ 'G"
  locale graph_delete_edge = graph +
    constrains α :: "'G ⇒ ('V,'W) graph"
    fixes delete_edge :: "'V ⇒ 'W ⇒ 'V ⇒ 'G ⇒ 'G"
    assumes delete_edge_correct:
      "invar g ⟹ invar (delete_edge v e v' g)"
      "invar g ⟹ α (delete_edge v e v' g) = Graph.delete_edge v e v' (α g)"

  type_synonym ('V,'W,'σ,'G) graph_nodes_it = "'G ⇒ ('V,'σ) set_iterator"

  locale graph_nodes_it_defs =
    fixes nodes_list_it :: "'G ⇒ ('V,'V list) set_iterator"
  begin
    definition "nodes_it g ≡ it_to_it (nodes_list_it g)"
  end

  locale graph_nodes_it = graph α invar + graph_nodes_it_defs nodes_list_it 
    for α :: "'G ⇒ ('V,'W) graph" and invar and
    nodes_list_it :: "'G ⇒ ('V,'V list) set_iterator"
    +
    assumes nodes_list_it_correct:
      "invar g ⟹ set_iterator (nodes_list_it g) (Graph.nodes (α g))"
  begin
    lemma nodes_it_correct: 
      "invar g ⟹ set_iterator (nodes_it g) (Graph.nodes (α g))"
      unfolding nodes_it_def
      apply (rule it_to_it_correct)
      by (rule nodes_list_it_correct)

    lemma pi_nodes_it[icf_proper_iteratorI]: 
      "proper_it (nodes_it S) (nodes_it S)"
      unfolding nodes_it_def 
      by (intro icf_proper_iteratorI)

    lemma nodes_it_proper[proper_it]:
      "proper_it' nodes_it nodes_it"
      apply (rule proper_it'I)
      by (rule pi_nodes_it)

  end

  type_synonym ('V,'W,'σ,'G) graph_edges_it 
    = "'G ⇒ (('V×'W×'V),'σ) set_iterator"

  locale graph_edges_it_defs =
    fixes edges_list_it :: "('V,'W,('V×'W×'V) list,'G) graph_edges_it"
  begin
    definition "edges_it g ≡ it_to_it (edges_list_it g)"
  end

  locale graph_edges_it = graph α invar + graph_edges_it_defs edges_list_it
    for α :: "'G ⇒ ('V,'W) graph" and invar and
    edges_list_it :: "('V,'W,('V×'W×'V) list,'G) graph_edges_it" 
    +
    assumes edges_list_it_correct:
      "invar g ⟹ set_iterator (edges_list_it g) (Graph.edges (α g))"
  begin
    lemma edges_it_correct: 
      "invar g ⟹ set_iterator (edges_it g) (Graph.edges (α g))"
      unfolding edges_it_def
      apply (rule it_to_it_correct)
      by (rule edges_list_it_correct)

    lemma pi_edges_it[icf_proper_iteratorI]: 
      "proper_it (edges_it S) (edges_it S)"
      unfolding edges_it_def 
      by (intro icf_proper_iteratorI)

    lemma edges_it_proper[proper_it]:
      "proper_it' edges_it edges_it"
      apply (rule proper_it'I)
      by (rule pi_edges_it)

  end

  type_synonym ('V,'W,'σ,'G) graph_succ_it = 
    "'G ⇒ 'V ⇒ ('W×'V,'σ) set_iterator"

  locale graph_succ_it_defs =
    fixes succ_list_it :: "'G ⇒ 'V ⇒ ('W×'V,('W×'V) list) set_iterator"
  begin
    definition "succ_it g v ≡ it_to_it (succ_list_it g v)"
  end

  locale graph_succ_it = graph α invar + graph_succ_it_defs succ_list_it
    for α :: "'G ⇒ ('V,'W) graph" and invar and
    succ_list_it :: "'G ⇒ 'V ⇒ ('W×'V,('W×'V) list) set_iterator" +
    assumes succ_list_it_correct:
      "invar g ⟹ set_iterator (succ_list_it g v) (Graph.succ (α g) v)"
  begin
    lemma succ_it_correct: 
      "invar g ⟹ set_iterator (succ_it g v) (Graph.succ (α g) v)"
      unfolding succ_it_def
      apply (rule it_to_it_correct)
      by (rule succ_list_it_correct)

    lemma pi_succ_it[icf_proper_iteratorI]: 
      "proper_it (succ_it S v) (succ_it S v)"
      unfolding succ_it_def 
      by (intro icf_proper_iteratorI)

    lemma succ_it_proper[proper_it]:
      "proper_it' (λS. succ_it S v) (λS. succ_it S v)"
      apply (rule proper_it'I)
      by (rule pi_succ_it)

  end

  subsection "Adjacency Lists"
  type_synonym ('V,'W) adj_list = "'V list × ('V×'W×'V) list"

  definition adjl_α :: "('V,'W) adj_list ⇒ ('V,'W) graph" where
    "adjl_α l ≡ let (nl,el) = l in ⦇
      nodes = set nl ∪ fst`set el ∪ snd`snd`set el,
      edges = set el
    ⦈"

  (* TODO: Do we have naming conventions for such a lemma ? *)
  lemma adjl_is_graph: "graph adjl_α (λ_. True)"
    apply (unfold_locales)
    unfolding adjl_α_def
    by force+

  type_synonym ('V,'W,'G) graph_from_list = "('V,'W) adj_list ⇒ 'G"
  locale graph_from_list = graph +
    constrains α :: "'G ⇒ ('V,'W) graph"
    fixes from_list :: "('V,'W) adj_list ⇒ 'G"
    assumes from_list_correct:
      "invar (from_list l)"
      "α (from_list l) = adjl_α l"

  type_synonym ('V,'W,'G) graph_to_list = "'G ⇒ ('V,'W) adj_list"
  locale graph_to_list = graph +
    constrains α :: "'G ⇒ ('V,'W) graph"
    fixes to_list :: "'G ⇒ ('V,'W) adj_list"
    assumes to_list_correct:
      "invar g ⟹ adjl_α (to_list g) = α g"

  subsection ‹Record Based Interface›
  record ('V,'W,'G) graph_ops =
    gop_α :: "('V,'W,'G) graph_α"
    gop_invar :: "'G ⇒ bool"
    gop_empty :: "('V,'W,'G) graph_empty"
    gop_add_node :: "('V,'W,'G) graph_add_node"
    gop_delete_node :: "('V,'W,'G) graph_delete_node"
    gop_add_edge :: "('V,'W,'G) graph_add_edge"
    gop_delete_edge :: "('V,'W,'G) graph_delete_edge"
    gop_from_list :: "('V,'W,'G) graph_from_list"
    gop_to_list :: "('V,'W,'G) graph_to_list"
    gop_nodes_list_it :: "'G ⇒ ('V,'V list) set_iterator"
    gop_edges_list_it :: "('V,'W,('V×'W×'V) list,'G) graph_edges_it"
    gop_succ_list_it :: "'G ⇒ 'V ⇒ ('W×'V,('W×'V) list) set_iterator"    

  locale StdGraphDefs = 
    graph_nodes_it_defs "gop_nodes_list_it ops"
    + graph_edges_it_defs "gop_edges_list_it ops"
    + graph_succ_it_defs "gop_succ_list_it ops"
    for ops :: "('V,'W,'G,'m) graph_ops_scheme"
  begin
    abbreviation α where "α ≡ gop_α ops"
    abbreviation invar where "invar ≡ gop_invar ops"
    abbreviation empty where "empty ≡ gop_empty ops"
    abbreviation add_node where "add_node ≡ gop_add_node ops"
    abbreviation delete_node where "delete_node ≡ gop_delete_node ops"
    abbreviation add_edge where "add_edge ≡ gop_add_edge ops"
    abbreviation delete_edge where "delete_edge ≡ gop_delete_edge ops"
    abbreviation from_list where "from_list ≡ gop_from_list ops"
    abbreviation to_list where "to_list ≡ gop_to_list ops"
    abbreviation nodes_list_it where "nodes_list_it ≡ gop_nodes_list_it ops"
    abbreviation edges_list_it where "edges_list_it ≡ gop_edges_list_it ops"
    abbreviation succ_list_it  where "succ_list_it ≡ gop_succ_list_it ops"
  end

  locale StdGraph = StdGraphDefs +
    graph α invar +
    graph_empty α invar empty +
    graph_add_node α invar add_node +
    graph_delete_node α invar delete_node +
    graph_add_edge α invar add_edge +
    graph_delete_edge α invar delete_edge +
    graph_from_list α invar from_list +
    graph_to_list α invar to_list +
    graph_nodes_it α invar nodes_list_it +
    graph_edges_it α invar edges_list_it +
    graph_succ_it α invar succ_list_it
  begin
    lemmas correct = empty_correct add_node_correct delete_node_correct 
      add_edge_correct delete_edge_correct
      from_list_correct to_list_correct 

  end

  subsection ‹Refinement Framework Bindings›
  lemma (in graph_nodes_it) nodes_it_is_iterator[refine_transfer]:
    "invar g ⟹ set_iterator (nodes_it g) (nodes (α g))"
    by (rule nodes_it_correct)

  lemma (in graph_edges_it) edges_it_is_iterator[refine_transfer]:
    "invar g ⟹ set_iterator (edges_it g) (edges (α g))"
    by (rule edges_it_correct)
    
  lemma (in graph_succ_it) succ_it_is_iterator[refine_transfer]:
    "invar g ⟹ set_iterator (succ_it g v) (Graph.succ (α g) v)"
    by (rule succ_it_correct)

  lemma (in graph) drh[refine_dref_RELATES]: "RELATES (build_rel α invar)"
    by (simp add: RELATES_def)

  (*text {* Autodet bindings: *}

  lemma (in graph_nodes_it) graph_nodes_it_t[trans_uc]:
    "DETREFe g (build_rel α invar) g' ⟹ 
      set_iterator (nodes_it g) (nodes g')"
    using nodes_it_correct by auto

  lemma (in graph_succ_it) graph_succ_it_t[trans_uc]:
    "DETREFe g (build_rel α invar) g' ⟹ DETREFe v Id v' ⟹
      set_iterator (succ_it g v) (succ g' v')"
    using succ_it_correct by auto

  lemma (in graph_edges_it) graph_edges_it_t[trans_uc]:
    "DETREFe g (build_rel α invar) g' ⟹ 
      set_iterator (edges_it g) (edges g')"
    using edges_it_correct by auto*)

end