Theory Shortest_SCC_Paths

theory Shortest_SCC_Paths
  imports Gabow_SCC.Gabow_SCC_Code
begin

definition compute_SCC_tr ::
  "('a :: hashable ⇒ bool, 'a ⇒ 'a list, 'a list, 'b) gen_g_impl_scheme ⇒ _" where
  "compute_SCC_tr =
    Gabow_SCC_Code.compute_SCC_tr (=) bounded_hashcode_nat (def_hashmap_size TYPE('a))"

― ‹Example usage:›
term "compute_SCC_tr ⦇ gi_V = (λ x. True), gi_E = (λ x. [3]), gi_V0 = [1], … = 3 ⦈"

text ‹
  Efficiently calculate shortest paths in a graph with non-negative edge weights,
  and where the only cycles are 0-cycles.
›
definition
"calc_shortest_scc_paths G n ≡
let
  sccs = compute_SCC_tr G;
  d = replicate n None @ [Some 0];
  d = (
    fold
      (λ vs d.
        fold
          (λ u d.
            fold
              (λ v d.
                case d ! u of
                  None ⇒ d
                | Some du ⇒ (
                  case d ! v of
                    None ⇒ d[v := Some (du + more G u v)]
                  | Some dv ⇒
                      if du + more G u v < dv
                      then d[v := Some (du + more G u v)]
                      else d
                  )
              )
              (gi_E G u)
              d
          )
          vs
          d
      )
      sccs
      d
  );
  d = (
    fold
      (λ vs d.
        let
          dscc =
            fold
            (λ v dscc.
              case dscc of
                None ⇒ d ! v
              | Some d' ⇒ (
                  case d ! v of
                    None ⇒ dscc
                  | Some dv ⇒ Some (min dv d')
                )
            )
            vs
            None
        in
          fold (λ v d. d[v:=dscc]) vs d
      )
      sccs
      d
  )
in d
"

end