Theory Graph

header {* Graphs *}
theory Graph
imports Main
begin
text {*
  This theory defines a notion of graphs. A graph is a record that
  contains a set of nodes @{text "V"} and a set of labeled edges 
  @{text "E ⊆ V×W×V"}, where @{text "W"} are the edge labels.
*}

subsection {* Definitions *}
  text {* A graph is represented by a record. *}
  record ('v,'w) graph =
    nodes :: "'v set"
    edges :: "('v × 'w × 'v) set"

  text {* In a valid graph, edges only go from nodes to nodes. *}
  locale valid_graph = 
    fixes G :: "('v,'w) graph"
    assumes E_valid: "fst`edges G ⊆ nodes G"
                     "snd`snd`edges G ⊆ nodes G"
  begin
    abbreviation "V ≡ nodes G"
    abbreviation "E ≡ edges G"

    lemma E_validD: assumes "(v,e,v')∈E"
      shows "v∈V" "v'∈V"
      apply -
      apply (rule set_mp[OF E_valid(1)])
      using assms apply force
      apply (rule set_mp[OF E_valid(2)])
      using assms apply force
      done

  end

  subsection {* Basic operations on Graphs *}

  text {* The empty graph. *}
  definition empty where 
    "empty ≡ (| nodes = {}, edges = {} |)),"
  text {* Adds a node to a graph. *}
  definition add_node where 
    "add_node v g ≡ (| nodes = insert v (nodes g), edges=edges g|)),"
  text {* Deletes a node from a graph. Also deletes all adjacent edges. *}
  definition delete_node where "delete_node v g ≡ (| 
    nodes = nodes g - {v},   
    edges = edges g ∩ (-{v})×UNIV×(-{v})
    |)),"
  text {* Adds an edge to a graph. *}
  definition add_edge where "add_edge v e v' g ≡ (|
    nodes = {v,v'} ∪ nodes g,
    edges = insert (v,e,v') (edges g)
    |)),"
  text {* Deletes an edge from a graph. *}
  definition delete_edge where "delete_edge v e v' g ≡ (|
    nodes = nodes g, edges = edges g - {(v,e,v')} |)),"
  text {* Successors of a node. *}
  definition succ :: "('v,'w) graph => 'v => ('w×'v) set"
    where "succ G v ≡ {(w,v'). (v,w,v')∈edges G}"

  text {* Now follow some simplification lemmas. *}
  lemma empty_valid[simp]: "valid_graph empty"
    unfolding empty_def by unfold_locales auto
  lemma add_node_valid[simp]: assumes "valid_graph g" 
    shows "valid_graph (add_node v g)"
  proof -
    interpret valid_graph g by fact
    show ?thesis
      unfolding add_node_def 
      by unfold_locales (auto dest: E_validD)
  qed
  lemma delete_node_valid[simp]: assumes "valid_graph g" 
    shows "valid_graph (delete_node v g)"
  proof -
    interpret valid_graph g by fact
    show ?thesis
      unfolding delete_node_def 
      by unfold_locales (auto dest: E_validD)
  qed
  lemma add_edge_valid[simp]: assumes "valid_graph g" 
    shows "valid_graph (add_edge v e v' g)"
  proof -
    interpret valid_graph g by fact
    show ?thesis
      unfolding add_edge_def
      by unfold_locales (auto dest: E_validD)
  qed
  lemma delete_edge_valid[simp]: assumes "valid_graph g" 
    shows "valid_graph (delete_edge v e v' g)"
  proof -
    interpret valid_graph g by fact
    show ?thesis
      unfolding delete_edge_def
      by unfold_locales (auto dest: E_validD)
  qed

  lemma succ_finite[simp, intro]: "finite (edges G) ==> finite (succ G v)"
    unfolding succ_def
    by (rule finite_subset[where B="snd`edges G"]) force+

  lemma nodes_empty[simp]: "nodes empty = {}" unfolding empty_def by simp
  lemma edges_empty[simp]: "edges empty = {}" unfolding empty_def by simp
  lemma succ_empty[simp]: "succ empty v = {}" unfolding empty_def succ_def by auto

  lemma nodes_add_node[simp]: "nodes (add_node v g) = insert v (nodes g)"
    by (simp add: add_node_def)
  lemma nodes_add_edge[simp]: 
    "nodes (add_edge v e v' g) = insert v (insert v' (nodes g))"
    by (simp add: add_edge_def)
  lemma edges_add_edge[simp]: 
    "edges (add_edge v e v' g) = insert (v,e,v') (edges g)"
    by (simp add: add_edge_def)
  lemma edges_add_node[simp]: 
    "edges (add_node v g) = edges g"
    by (simp add: add_node_def)

  lemma (in valid_graph) succ_subset: "succ G v ⊆ UNIV×V"
    unfolding succ_def using E_valid
    by (force)

subsection {* Paths *}
  text {* A path is represented by a list of adjacent edges. *}
  type_synonym ('v,'w) path = "('v×'w×'v) list"

  context valid_graph
  begin
    text {* The following predicate describes a valid path: *}
    fun is_path :: "'v => ('v,'w) path => 'v => bool" where
      "is_path v [] v' <-> v=v' ∧ v'∈V" |
      "is_path v ((v1,w,v2)#p) v' <-> v=v1 ∧ (v1,w,v2)∈E ∧ is_path v2 p v'"
  
    lemma is_path_simps[simp, intro!]:
      "is_path v [] v <-> v∈V"
      "is_path v [(v,w,v')] v' <-> (v,w,v')∈E"
      by (auto dest: E_validD)
    
    lemma is_path_memb[simp]:
      "is_path v p v' ==> v∈V ∧ v'∈V"
      apply (induct p arbitrary: v) 
      apply (auto dest: E_validD)
      done

    lemma is_path_split:
      "is_path v (p1@p2) v' <-> (∃u. is_path v p1 u ∧ is_path u p2 v')"
      by (induct p1 arbitrary: v) auto

    lemma is_path_split'[simp]: 
      "is_path v (p1@(u,w,u')#p2) v' 
        <-> is_path v p1 u ∧ (u,w,u')∈E ∧ is_path u' p2 v'"
      by (auto simp add: is_path_split)
  end

  text {* Set of intermediate vertices of a path. These are all vertices but
    the last one. Note that, if the last vertex also occurs earlier on the path,
    it is contained in @{text "int_vertices"}. *}
  definition int_vertices :: "('v,'w) path => 'v set" where
    "int_vertices p ≡ set (map fst p)"

  lemma int_vertices_simps[simp]:
    "int_vertices [] = {}"
    "int_vertices (vv#p) = insert (fst vv) (int_vertices p)"
    "int_vertices (p1@p2) = int_vertices p1 ∪ int_vertices p2"
    by (auto simp add: int_vertices_def)
  
  lemma (in valid_graph) int_vertices_subset: 
    "is_path v p v' ==> int_vertices p ⊆ V"
    apply (induct p arbitrary: v)
    apply (simp) 
    apply (force dest: E_validD)
    done

  lemma int_vertices_empty[simp]: "int_vertices p = {} <-> p=[]"
    by (cases p) auto

subsubsection {* Splitting Paths *}
  text {*Split a path at the point where it first leaves the set @{text W}: *}
  lemma (in valid_graph) path_split_set:
    assumes "is_path v p v'" and "v∈W" and "v'∉W"
    obtains p1 p2 u w u' where
    "p=p1@(u,w,u')#p2" and
    "int_vertices p1 ⊆ W" and "u∈W" and "u'∉W"
    using assms
  proof (induct p arbitrary: v thesis)
    case Nil thus ?case by auto
  next
    case (Cons vv p)
    note [simp, intro!] = `v∈W` `v'∉W`
    from Cons.prems obtain w u' where 
      [simp]: "vv=(v,w,u')" and
        REST: "is_path u' p v'"
      by (cases vv) auto
    
    txt {* Distinguish wether the second node @{text u'} of the path is 
      in @{text W}. If yes, the proposition follows by the 
      induction hypothesis, otherwise it is straightforward, as
      the split takes place at the first edge of the path. *}
    {
      assume A [simp, intro!]: "u'∈W"
      from Cons.hyps[OF _ REST] obtain p1 uu ww uu' p2 where
        "p=p1@(uu,ww,uu')#p2" "int_vertices p1 ⊆ W" "uu ∈ W" "uu' ∉ W"
        by blast
      with Cons.prems(1)[of "vv#p1" uu ww uu' p2] have thesis by auto
    } moreover {
      assume "u'∉W"
      with Cons.prems(1)[of "[]" v w u' p] have thesis by auto
    } ultimately show thesis by blast
  qed
  
  text {*Split a path at the point where it first enters the set @{text W}:*}
  lemma (in valid_graph) path_split_set':
    assumes "is_path v p v'" and "v'∈W"
    obtains p1 p2 u where
    "p=p1@p2" and
    "is_path v p1 u" and
    "is_path u p2 v'" and
    "int_vertices p1 ⊆ -W" and "u∈W"
    using assms
  proof (cases "v∈W")
    case True with that[of "[]" p] assms show ?thesis
      by auto
  next
    case False with assms that show ?thesis
    proof (induct p arbitrary: v thesis)
      case Nil thus ?case by auto
    next
      case (Cons vv p)
      note [simp, intro!] = `v'∈W` `v∉W`
      from Cons.prems obtain w u' where 
        [simp]: "vv=(v,w,u')" and [simp]: "(v,w,u')∈E" and
          REST: "is_path u' p v'"
        by (cases vv) auto
    
      txt {* Distinguish wether the second node @{text u'} of the path is 
        in @{text W}. If yes, the proposition is straightforward, otherwise,
        it follows by the induction hypothesis.
        *}
      {
        assume A [simp, intro!]: "u'∈W"
        from Cons.prems(3)[of "[vv]" p u'] REST have ?case by auto
      } moreover {
        assume [simp, intro!]: "u'∉W"
        from Cons.hyps[OF REST] obtain p1 p2 u'' where
          [simp]: "p=p1@p2" and 
            "is_path u' p1 u''" and 
            "is_path u'' p2 v'" and
            "int_vertices p1 ⊆ -W" and
            "u''∈W" by blast
        with Cons.prems(3)[of "vv#p1"] have ?case by auto
      } ultimately show ?case by blast
    qed
  qed

  text {* Split a path at the point where a given vertex is first visited: *}
  lemma (in valid_graph) path_split_vertex:
    assumes "is_path v p v'" and "u∈int_vertices p"
    obtains p1 p2 where
    "p=p1@p2" and
    "is_path v p1 u" and
    "u ∉ int_vertices p1"
    using assms
  proof (induct p arbitrary: v thesis)
    case Nil thus ?case by auto
  next
    case (Cons vv p)
    from Cons.prems obtain w u' where 
      [simp]: "vv=(v,w,u')" "v∈V" "(v,w,u')∈E" and
        REST: "is_path u' p v'"
      by (cases vv) auto
    
    {
      assume "u=v"
      with Cons.prems(1)[of "[]" "vv#p"] have thesis by auto
    } moreover {
      assume [simp]: "u≠v"
      with Cons.hyps(1)[OF _ REST] Cons.prems(3) obtain p1 p2 where
        "p=p1@p2" "is_path u' p1 u" "u∉int_vertices p1"
        by auto
      with Cons.prems(1)[of "vv#p1" p2] have thesis
        by auto
    } ultimately show ?case by blast
  qed

subsection {* Weighted Graphs *}
  locale valid_mgraph = valid_graph G for G::"('v,'w::monoid_add) graph"

  definition path_weight :: "('v,'w::monoid_add) path => 'w"
    where "path_weight p ≡ listsum (map (fst o snd) p)"

  (* 
    lemma path_weight_alt: "path_weight p ≡ listsum (map (fst o snd) p)"
    unfolding path_weight_def foldl_conv_fold
    by (simp add: listsum_foldl)
  *)

  lemma path_weight_split[simp]:
    "(path_weight (p1@p2)::'w::monoid_add) = path_weight p1 + path_weight p2"
    unfolding path_weight_def
    by (auto)

  lemma path_weight_empty[simp]: "path_weight [] = 0"
    unfolding path_weight_def
    by auto

  lemma path_weight_cons[simp]:
    "(path_weight (e#p)::'w::monoid_add) = fst (snd e) + path_weight p"
    unfolding path_weight_def
    by (auto)

end