Theory GraphSpec

header "Graph Interface"
theory GraphSpec
imports Main Graph "../Refine_Monadic/Refine" 
  (*"../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 = graph +
    constrains α :: "'G => ('V,'W) graph"
    fixes nodes_it :: "'G => ('V,'σ) set_iterator"
    assumes nodes_it_correct:
      "invar g ==> set_iterator (nodes_it g) (Graph.nodes (α g))"

  type_synonym ('V,'W,'σ,'G) graph_edges_it 
    = "'G => (('V×'W×'V),'σ) set_iterator"
  locale graph_edges_it = graph +
    constrains α :: "'G => ('V,'W) graph"
    fixes edges_it :: "('V,'W,'σ,'G) graph_edges_it"
    assumes edges_it_correct:
      "invar g ==> set_iterator (edges_it g) (Graph.edges (α g))"

  type_synonym ('V,'W,'σ,'G) graph_succ_it = 
    "'G => 'V => ('W×'V,'σ) set_iterator"
  locale graph_succ_it = graph +
    constrains α :: "'G => ('V,'W) graph"
    fixes succ_it :: "'G => 'V => ('W×'V,'σ) set_iterator"
    assumes succ_it_correct:
      "invar g ==> set_iterator (succ_it g v) (Graph.succ (α g) v)"

  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"

  locale StdGraphDefs =
    fixes 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"
  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
  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