Theory Dijkstra_Shortest_Path.GraphGA

section ‹Generic Algorithms for Graphs›
theory GraphGA
imports 
  GraphSpec 
begin

  definition gga_from_list :: 
    "('V,'W,'G) graph_empty ⇒ ('V,'W,'G) graph_add_node 
      ⇒ ('V,'W,'G) graph_add_edge 
    ⇒ ('V,'W,'G) graph_from_list"
    where 
    "gga_from_list e a u l ≡ 
      let (nl,el) = l;
        g1 = foldl (λg v. a v g) (e ()) nl
      in foldl (λg (v,e,v'). u v e v' g) g1 el"
  
  lemma gga_from_list_correct:
    fixes α :: "'G ⇒ ('V,'W) graph"
    assumes "graph_empty α invar e"
    assumes "graph_add_node α invar a"
    assumes "graph_add_edge α invar u"
    shows "graph_from_list α invar (gga_from_list e a u)"
  proof -
    interpret 
      graph_empty α invar e + 
      graph_add_node α invar a + 
      graph_add_edge α invar u
      by fact+

    {
      fix nl el
      define g1 where "g1 = foldl (λg v. a v g) (e ()) nl"
      define g2 where "g2 = foldl (λg (v,e,v'). u v e v' g) g1 el"
      have "invar g1 ∧ α g1 = ⦇ nodes = set nl, edges = {} ⦈"
        unfolding g1_def
        by (induct nl rule: rev_induct)
           (auto simp: empty_correct add_node_correct empty_def add_node_def)
      hence "invar g2 
        ∧ α g2 = ⦇ nodes = set nl ∪ fst`set el ∪ snd`snd`set el,
                    edges = set el ⦈"
        unfolding g2_def
        by (induct el rule: rev_induct) (auto simp: add_edge_correct add_edge_def)
      hence "invar g2 ∧ adjl_α (nl,el) = α g2"
        unfolding adjl_α_def by auto
    }
    thus ?thesis
      unfolding gga_from_list_def [abs_def]
      apply unfold_locales
      apply auto
      done
  qed
      
  term map_iterator_product


  locale gga_edges_it_defs =
    graph_nodes_it_defs nodes_list_it +
    graph_succ_it_defs succ_list_it
    for nodes_list_it :: "('V,'W,'V list,'G) graph_nodes_it"
    and succ_list_it :: "('V,'W,('W×'V) list,'G) graph_succ_it"
  begin
    definition gga_edges_list_it ::
      "('V,'W,('V×'W×'V) list,'G) graph_edges_it"
      where "gga_edges_list_it G ≡ set_iterator_product 
        (nodes_it G) (succ_it G)"
    local_setup ‹Locale_Code.lc_decl_del @{term gga_edges_list_it}›
  end
  setup ‹
    (Record_Intf.add_unf_thms_global @{thms 
      gga_edges_it_defs.gga_edges_list_it_def[abs_def]
    })
› 

  locale gga_edges_it = gga_edges_it_defs nodes_list_it succ_list_it 
    + graph α invar
    + graph_nodes_it α invar nodes_list_it
    + graph_succ_it α invar succ_list_it
    for α :: "'G ⇒ ('V,'W) graph" 
    and invar 
    and nodes_list_it :: "('V,'W,'V list,'G) graph_nodes_it"
    and succ_list_it :: "('V,'W,('W×'V) list,'G) graph_succ_it"  
  begin
    lemma gga_edges_list_it_impl:
      shows "graph_edges_it α invar gga_edges_list_it"
    proof
      fix g
      assume INV: "invar g"

      from set_iterator_product_correct[OF 
        nodes_it_correct[OF INV] succ_it_correct[OF INV]]
      have "set_iterator (set_iterator_product (nodes_it g) (λv. succ_it g v))
        (SIGMA v:nodes (α g). succ (α g) v)
        " .
      also have "(SIGMA v:nodes (α g). succ (α g) v) = edges (α g)" 
        unfolding succ_def 
        by (auto dest: valid_graph.E_validD[OF valid[OF INV]])

      finally show "set_iterator (gga_edges_list_it g) (edges (α g))"
        unfolding gga_edges_list_it_def .
    qed
  end

  locale gga_to_list_defs_loc = 
    graph_nodes_it_defs nodes_list_it
    + graph_edges_it_defs edges_list_it
    for nodes_list_it :: "('V,'W,'V list,'G) graph_nodes_it"
    and edges_list_it :: "('V,'W,('V×'W×'V) list,'G) graph_edges_it"  
  begin
    definition gga_to_list :: 
      "('V,'W,'G) graph_to_list"
      where 
      "gga_to_list g ≡ 
        (nodes_it g (λ_. True) (#) [], edges_it g (λ_. True) (#) [])
      "
  end

  locale gga_to_list_loc = gga_to_list_defs_loc nodes_list_it edges_list_it +
    graph α invar 
    + graph_nodes_it α invar nodes_list_it
    + graph_edges_it α invar edges_list_it
    for α :: "'G ⇒ ('V,'W) graph" and invar
    and nodes_list_it :: "('V,'W,'V list,'G) graph_nodes_it"
    and edges_list_it :: "('V,'W,('V×'W×'V) list,'G) graph_edges_it"  
  begin

    lemma gga_to_list_correct:
      shows "graph_to_list α invar gga_to_list"
    proof 
      fix g
      assume [simp, intro!]: "invar g"
      then interpret valid_graph "α g" by (rule valid)

      have "set (nodes_it g (λ_. True) (#) []) = V"
        apply (rule_tac I="λit σ. set σ = V - it" 
          in set_iterator_rule_P[OF nodes_it_correct])
        by auto
      moreover have "set (edges_it g (λ_. True) (#) []) = E"
        apply (rule_tac I="λit σ. set σ = E - it" 
          in set_iterator_rule_P[OF edges_it_correct])
        by auto
      ultimately show "adjl_α (gga_to_list g) = α g"
        unfolding adjl_α_def gga_to_list_def
        apply simp
        apply (rule graph.equality)
        apply (auto intro: E_validD)
        done
    qed

  end

end