Theory GraphGA

header {* Generic Algorithms for Graphs *}
theory GraphGA
imports GraphSpec "../Collections/iterator/SetIteratorOperations"
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
      def g1≡"(foldl (λg v. a v g) (e ()) nl)"
      def 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

  definition gga_edges_it ::
    "('V,'W,'σ,'G) graph_nodes_it => ('V,'W,'σ,'G) graph_succ_it 
    => ('V,'W,'σ,'G) graph_edges_it"
    where "gga_edges_it ni si G ≡ set_iterator_product (ni G) (λv. si G v)"

(*
    "gga_edges_it ni si G c f σ0 ≡ 
      ni G c (
        λv σ. si G v c (λ(w,v') σ. f (v,w,v') σ) σ
      ) σ0
    "
*)

  lemma gga_edges_it_correct:
    fixes ni::"('V,'W,'σ,'G) graph_nodes_it"
    fixes α :: "'G => ('V,'W) graph"
    assumes "graph_nodes_it α invar ni"
    assumes "graph_succ_it α invar si"
    shows "graph_edges_it α invar (gga_edges_it ni si)"
  proof -
    interpret graph_nodes_it α invar ni +
      graph_succ_it α invar si by fact+

    show ?thesis
    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 (ni g) (λv. si 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_it ni si g) (edges (α g))"
        unfolding gga_edges_it_def .
    qed
  qed
        
  definition gga_to_list :: 
    "('V,'W,_,'G) graph_nodes_it => ('V,'W,_,'G) graph_edges_it => 
     ('V,'W,'G) graph_to_list"
    where 
    "gga_to_list ni ei g ≡ 
      (ni g (λ_. True) (op #) [], ei g (λ_. True) (op #) [])
    "

  lemma gga_to_list_correct:
    fixes α :: "'G => ('V,'W) graph"
    assumes "graph_nodes_it α invar ni"
    assumes "graph_edges_it α invar ei"
    shows "graph_to_list α invar (gga_to_list ni ei)"
  proof -
    interpret graph_nodes_it α invar ni + 
      graph_edges_it α invar ei
      by fact+

    show ?thesis
    proof 
      fix g
      assume [simp, intro!]: "invar g"
      then interpret valid_graph "α g" by (rule valid)

      have "set (ni g (λ_. True) (op #) []) = V"
        apply (rule_tac I="λit σ. set σ = V - it" 
          in set_iterator_rule_P[OF nodes_it_correct])
        by auto
      moreover have "set (ei g (λ_. True) (op #) []) = 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 ni ei g) = α g"
        unfolding adjl_α_def gga_to_list_def
        apply simp
        apply (rule graph.equality)
        apply (auto intro: E_validD)
        done
    qed
  qed

end