Theory NetCheck

section ‹Checking for Valid Network›
theory NetCheck
imports 
  "Lib/Refine_Add_Fofu"
  Network
  Graph_Impl
  DFS_Framework.Reachable_Nodes
begin
text ‹
  This theory contains code to read a network from an edge list, 
  and verify that the network is a valid input for the 
  Edmonds Karp Algorithm.
›

(*<*)
  declare [[coercion_delete int]]
  declare [[coercion_delete "real::nat⇒real"]]
(*>*)

  subsection ‹Graphs as Lists of Edges›
  text ‹Graphs can be represented as lists of edges, each edge being a triple of 
    start node, end node, and capacity. Capacities must be positive, and there
    must not be multiple edges with the same start and end node. ›

  type_synonym edge_list = "(node × node × capacity_impl) list"

  definition ln_invar :: "edge_list ⇒ bool" where 
    "ln_invar el ≡ 
      distinct (map (λ(u, v, _). (u,v)) el) 
    ∧ (∀(u,v,c)∈set el. c>0) 
    "
  definition ln_α :: "edge_list ⇒ capacity_impl graph" where 
    "ln_α el ≡ λ(u,v). 
      if ∃c. (u, v, c) ∈ set el ∧ c ≠ 0 then 
        SOME c. (u, v, c) ∈ set el ∧ c ≠ 0
      else 0"

  definition "ln_rel ≡ br ln_α ln_invar"
  
  lemma ln_equivalence: "(el, c') ∈ ln_rel ⟷ ln_invar el ∧ c' = ln_α el"
    unfolding ln_rel_def br_def by auto 

  definition ln_N :: "(node×node×_) list ⇒ nat" 
    ― ‹Maximum node number plus one. I.e. the size of an array to be indexed by nodes.›
    where "ln_N el ≡ Max ((fst`set el) ∪ ((fst o snd)`set el)) + 1"

  lemma ln_α_imp_in_set: "⟦ln_α el (u,v)≠(0)⟧ ⟹ (u,v,ln_α el (u,v))∈set el"
    apply (auto simp: ln_α_def split: if_split_asm)
    apply (metis (mono_tags, lifting) someI_ex)
    done

  lemma ln_N_correct: "Graph.V (ln_α el) ⊆ {0..<ln_N el}"  
    apply (clarsimp simp: Graph.V_def Graph.E_def)
    apply (safe dest!: ln_α_imp_in_set)
    apply (fastforce simp: ln_N_def less_Suc_eq_le intro: Max_ge)
    apply (force simp: ln_N_def less_Suc_eq_le intro: Max_ge)
    done

  subsection ‹Pre-Networks›  
  text ‹This data structure is used to convert an edge-list to a network and 
    check validity. It maintains additional information, like a adjacency maps. ›

  record pre_network =
    pn_c :: "capacity_impl graph"
    pn_V :: "nat set"
    pn_succ :: "nat ⇒ nat list"
    pn_pred :: "nat ⇒ nat list"
    pn_adjmap :: "nat ⇒ nat list"
    pn_s_node :: bool
    pn_t_node :: bool

  fun read :: "edge_list ⇒ nat ⇒ nat ⇒ pre_network option" 
    ― ‹Read a pre-network from an edge list, and source/sink node numbers.›
  where
    "read [] _ _ = Some ⦇
      pn_c = (λ _. 0), 
      pn_V = {}, 
      pn_succ = (λ _. []),
      pn_pred = (λ _. []),
      pn_adjmap = (λ _. []), 
      pn_s_node = False, 
      pn_t_node = False
    ⦈"
  | "read ((u, v, c) # es) s t = ((case (read es s t) of 
      Some x ⇒
        (if (pn_c x) (u, v) = 0 ∧ (pn_c x) (v, u) = 0 ∧ c > 0 then
          (if u = v ∨ v = s ∨ u = t then
            None
          else
            Some (x⦇ 
              pn_c := (pn_c x) ((u, v) := c),
              pn_V := insert u (insert v (pn_V x)),
              pn_succ := (pn_succ x) (u := v # ((pn_succ x) u)),
              pn_pred := (pn_pred x) (v := u # ((pn_pred x) v)),
              pn_adjmap := (pn_adjmap x) (
                u := v # (pn_adjmap x) u, 
                v := u # (pn_adjmap x) v),
              pn_s_node := pn_s_node x ∨ u = s,
              pn_t_node := pn_t_node x ∨ v = t
            ⦈))
        else
          None)
    | None ⇒ None))"
      
  (* TODO: These proofs look overly verbose. *)  
  lemma read_correct1: "read es s t = Some ⦇pn_c = c, pn_V = V, pn_succ = succ, 
    pn_pred = pred , pn_adjmap = adjmap, pn_s_node = s_n, pn_t_node = t_n⦈ ⟹ 
    (es, c) ∈ ln_rel ∧ Graph.V c = V ∧ finite V ∧ 
    (s_n ⟶ s ∈ V) ∧ (t_n ⟶ t ∈ V) ∧ (¬s_n ⟶ s ∉ V) ∧ (¬t_n ⟶ t ∉ V) ∧
    (∀u v. c (u,v) ≥ 0) ∧
    (∀u. c(u, u) = 0) ∧ (∀u. c (u, s) = 0) ∧ (∀u. c (t, u) = 0) ∧
    (∀u v. c (u, v) ≠ 0 ⟶ c (v, u) = 0) ∧ 
    (∀u. set (succ u) = Graph.E c``{u} ∧ distinct (succ u)) ∧ 
    (∀u. set (pred u) = (Graph.E c)¯``{u} ∧ distinct (pred u)) ∧ 
    (∀u. set (adjmap u) = Graph.E c``{u} ∪ (Graph.E c)¯``{u} 
      ∧ distinct (adjmap u))"
    proof (induction es arbitrary: c V succ pred adjmap s_n t_n)
      case Nil
        thus ?case 
          unfolding Graph.V_def Graph.E_def ln_rel_def br_def 
            ln_α_def ln_invar_def 
          by auto
    next
      case (Cons e es)
        obtain u1 v1 c1 where obt1: "e = (u1, v1, c1)" by (meson prod_cases3)
        obtain x where obt2: "read es s t = Some x"
          using Cons.prems obt1 by (auto split: option.splits)
        have fct0: "(pn_c x) (u1, v1) = 0 ∧ (pn_c x) (v1, u1) = 0 ∧ c1 > 0"
          using Cons.prems obt1 obt2 by (auto split: option.splits if_splits)
        have fct1: "c1 > 0 ∧ u1 ≠ v1 ∧ v1 ≠ s ∧ u1 ≠ t"
          using Cons.prems obt1 obt2 by (auto split: option.splits if_splits)
        
        obtain c' V' sc' ps' pd' s_n' t_n' where obt3: 
          "x = ⦇pn_c = c', pn_V = V',
                pn_succ = sc', pn_pred = pd',  pn_adjmap = ps', 
                pn_s_node = s_n', pn_t_node = t_n'⦈" 
          apply (cases x) by auto
        then have "read es s t = Some ⦇pn_c = c', pn_V = V', 
          pn_succ = sc', pn_pred = pd',
          pn_adjmap = ps', pn_s_node = s_n', pn_t_node = t_n'⦈" 
          using obt2 by blast
        note fct = Cons.IH[OF this]
        have fct2: "s_n = (s_n' ∨ u1 = s)" 
          using fct0 fct1 Cons.prems obt1 obt2 obt3 by simp
        have fct3: "t_n = (t_n' ∨ v1 = t)"
          using fct0 fct1 Cons.prems obt1 obt2 obt3 by simp
        have fct4: "c = c' ((u1, v1) := c1)"
          using fct0 fct1 Cons.prems obt1 obt2 obt3 by simp
        have fct5: "V = V' ∪ {u1, v1}" 
          using fct0 fct1 Cons.prems obt1 obt2 obt3 by simp
        have fct6: "succ = sc' (u1 := v1 # sc' u1)" 
          using fct0 fct1 Cons.prems obt1 obt2 obt3 by simp
        have fct7: "pred = pd' (v1 := u1 # pd' v1)"
          using fct0 fct1 Cons.prems obt1 obt2 obt3 by simp
        have fct8: "adjmap = (ps' (u1 := v1 # ps' u1)) (v1 := u1 # ps' v1)"
          using fct0 fct1 Cons.prems obt1 obt2 obt3 by simp
        
          
        {
          have "(es, c') ∈ ln_rel" using fct by blast
          then have "ln_invar es" and "c' = ln_α es" 
            unfolding ln_rel_def br_def by auto
          
          have "ln_invar (e # es)"
            proof (rule ccontr)
              assume "¬ ?thesis"
              have f1: "∀(u, v, c) ∈ set (e # es). c>0" 
                using ‹ln_invar es› fct0 obt1
                unfolding ln_invar_def by auto
              have f2: "distinct (map (λ(u, v, _). (u,v)) es)" 
                using ‹ln_invar es›
                unfolding ln_invar_def by auto
              
              have "∃c1'. (u1, v1, c1') ∈ (set es) ∧ c1' ≠ 0"
                proof (rule ccontr)
                  assume "¬ ?thesis"
                  then have "∀c1'. (u1, v1, c1') ∉ (set es) ∨ c1' = 0" by blast
                  then have "distinct (map (λ(u, v, _). (u,v)) (e # es))" 
                    using obt1 f2 f1 by auto
                  then have "ln_invar (e # es)" 
                    unfolding ln_invar_def using f1 by simp
                  thus "False" using ‹¬ ln_invar (e # es)› by blast
                qed
              then obtain c1' where "(u1, v1, c1') ∈ (set es) ∧ c1' ≠ 0" 
                by blast
              then have "c' (u1, v1) = (SOME c. (u1, v1, c) ∈ set es ∧ c ≠ 0)"
                using ‹c' = ln_α es› unfolding ln_α_def by auto
              then have "c' (u1, v1) ≠ 0" 
                using ‹(u1, v1, c1') ∈ (set es) ∧ c1' ≠ 0› f1
                by (metis (mono_tags, lifting) tfl_some)
              thus "False" using fct0 obt3 by simp
            qed
          moreover {
            {
              fix a
              have f1: "distinct (map (λ(u, v, _). (u,v)) (e # es))"
                and f2: "∀u v. (u, v, 0) ∉ set (e # es)"
                using ‹ln_invar (e # es)› unfolding ln_invar_def by auto
              have "c a = ln_α (e # es) a"
                proof (cases "a = (u1, v1)")
                  case True
                    have "c a = c1" using fct4 True by simp
                    moreover {
                      have "(ln_α (e # es)) a 
                        = (SOME c. (u1, v1, c) ∈ set (e # es) ∧ c ≠ 0)"
                        (is "?L = ?R") 
                        unfolding ln_α_def using obt1 fct0 True by auto
                      moreover have "?R = c1"
                        proof (rule ccontr)
                          assume "¬ ?thesis"
                          then obtain c1' where 
                            "(u1, v1, c1') ∈ set (e # es) ∧ c1' ≠ 0 ∧ c1' ≠ c1" 
                            using fct0 obt1 by auto
                          then have 
                            "¬distinct (map (λ(u, v, _). (u,v)) (e # es))" 
                            using obt1 
                            by (metis (mono_tags, lifting) Pair_inject 
                              distinct_map_eq list.set_intros(1) split_conv) 
                          thus "False" using f1 by blast
                        qed
                      ultimately have "?L = c1" by blast
                    }
                    ultimately show ?thesis by simp
                next
                  case False
                    have f1: 
                      "∀u1' v1' c1'. u1' ≠ u1 ∨ v1' ≠ v1 
                      ⟶ ((u1', v1', c1') ∈ set (e # es)
                            ⟷ (u1', v1', c1') ∈ set es)" 
                      using obt1 by auto
                    obtain u1' v1' where "a = (u1', v1')" by (cases a)
                    {
                      have "(ln_α (e # es)) (u1', v1') = (ln_α es) (u1', v1')"
                        proof (cases 
                            "∃ c1'. (u1', v1', c1') ∈ set (e # es) ∧ c1' ≠ 0")
                          case True
                            thus ?thesis unfolding ln_α_def 
                              using f1 False True ‹a = (u1', v1')› by auto
                        next
                          case False
                            thus ?thesis unfolding ln_α_def by auto
                        qed
                      then have "(ln_α (e # es)) a = (ln_α es) a" 
                        using ‹a = (u1', v1')› by simp
                    }
                    moreover have "c a = c' a" using False fct4 by simp
                    moreover have "c' a = ln_α es a" using ‹c' = ln_α es› 
                      by simp
                    ultimately show ?thesis by simp
                qed
            }
            then have "c = ln_α (e # es)" by auto
          }
          ultimately have "(e # es, c) ∈ ln_rel" unfolding ln_rel_def br_def 
            by simp
        }
        moreover {
          have "Graph.V c = Graph.V c' ∪ {u1, v1}" 
            unfolding Graph.V_def Graph.E_def using fct0 fct4 by auto
          moreover have "Graph.V c' = V'" using fct by blast
          ultimately have "Graph.V c = V" using fct5 by auto
        }
        moreover {
          have "finite V'" using fct by blast
          then have "finite V" using fct5 by auto
        }
        moreover {
          assume "s_n"
          then have "s_n' ∨ u1 = s" using fct2 by blast
          then have "s ∈ V"
            proof
              assume "s_n'"
                thus ?thesis using fct fct5 by auto
            next
              assume "u1 = s"
                thus ?thesis using fct5 by simp
            qed
        }
        moreover {
          assume "t_n"
          then have "t_n' ∨ v1 = t" using fct3 by blast
          then have "t ∈ V"
            proof
              assume "t_n'"
                thus ?thesis using fct fct5 by auto
            next
              assume "v1 = t"
                thus ?thesis using fct5 by simp
            qed
        }
        moreover {
          assume "¬s_n"
          then have "¬s_n' ∧ u1 ≠ s" using fct2 by blast
          then have "s ∉ V" using fct fct5 fct1  by auto
        }
        moreover {
          assume "¬t_n"
          then have "¬t_n' ∧ v1 ≠ t" using fct3 by blast
          then have "t ∉ V" using fct fct5 fct1  by auto
        }
        moreover have "∀u v. (c (u, v) ≥ 0)" using fct fct4 fct1 fct0 by auto
        moreover have "∀u. c (u, u) = 0" using fct fct4 fct1 fct0 by auto
        moreover have "∀u. c (u, s) = 0" using fct fct4 fct1 fct0 by auto
        moreover have "∀u. c (t, u) = 0" using fct fct4 fct1 fct0 by auto
        moreover {
          fix a b
          assume "c (a, b) ≠ 0"
          then have "a ≠ b" using ‹∀u. c (u, u) = 0› by auto
          have "c (b, a) = 0"
            proof (cases "(a, b) = (u1, v1)")
              case True
                then have "c (b, a) = c' (v1, u1)" using fct4 ‹a ≠ b› by auto 
                moreover have "c' (v1, u1) = 0" using fct0 obt3 by auto
                ultimately show ?thesis by simp
            next
              case False
                thus ?thesis
                  proof (cases "(b, a) = (u1, v1)")
                    case True
                      then have "c (a, b) = c' (v1, u1)" using fct4 ‹a ≠ b› 
                        by auto
                      moreover have "c' (v1, u1) = 0" using fct0 obt3 by auto
                      ultimately show ?thesis using ‹c (a, b) ≠ 0› by simp
                  next
                    case False
                      then have "c (b, a) = c' (b, a)" using fct4 by auto
                      moreover have "c (a, b) = c' (a, b)" 
                        using False ‹(a, b) ≠ (u1, v1)› fct4 by auto
                      ultimately show ?thesis using fct ‹c (a, b) ≠ 0› by auto 
                  qed
            qed
        } note n_fct = this
        moreover {
          {
            fix a
            assume "a ≠ u1"
            then have "succ a = sc' a" using fct6 by simp
            moreover have "set (sc' a) = Graph.E c' `` {a} ∧ distinct (sc' a)"
              using fct by blast
            ultimately have "set (succ a) = Graph.E c``{a} ∧ distinct (succ a)"
              unfolding Graph.E_def using fct4 ‹a ≠ u1› by auto 
          }
          moreover {
            fix a
            assume "a = u1"
            have "set (succ a) = Graph.E c``{a} ∧ distinct (succ a)"
              proof (cases "c' (u1, v1) = 0")
                case True
                  have fct: "set (sc' a) = Graph.E c' `` {a} ∧ distinct (sc' a)"
                    using fct by blast
                  
                  have "succ a = v1 # sc' a" using ‹a = u1› fct6 True by simp
                  moreover have "Graph.E c = Graph.E c' ∪ {(u1, v1)}" 
                    unfolding Graph.E_def using fct4 fct0 by auto
                  moreover have "v1 ∉ set (sc' a)"
                    proof (rule ccontr)
                      assume "¬ ?thesis"
                      then have "c' (a, v1) ≠ 0" 
                        using fct unfolding Graph.E_def by auto
                      thus "False" using True ‹a = u1› by simp
                    qed
                  ultimately show ?thesis using ‹a = u1› fct by auto
              next
                case False
                  thus ?thesis using fct0 obt3 by auto
              qed
        }
        ultimately have 
          "∀u. set (succ u) = Graph.E c `` {u} ∧ distinct (succ u)" 
          by metis
      }
        moreover {
          {
            fix a
            assume "a ≠ v1"
            then have "pred a = pd' a" using fct7 by simp
            moreover have 
              "set (pd' a) = (Graph.E c')¯ `` {a} ∧ distinct (pd' a)"
              using fct by blast
            ultimately have 
              "set (pred a) = (Graph.E c)¯``{a} ∧ distinct (pred a)"
              unfolding Graph.E_def using fct4 ‹a ≠ v1› by auto 
          }
          moreover {
            fix a
            assume "a = v1"
            have "set (pred a) = (Graph.E c)¯``{a} ∧ distinct (pred a)"
              proof (cases "c' (u1, v1) = 0")
                case True
                  have fct: 
                    "set (pd' a) = (Graph.E c')¯ `` {a} ∧ distinct (pd' a)"
                    using fct by blast
                  
                  have "pred a = u1 # pd' a" using ‹a = v1› fct7 True by simp
                  moreover have "Graph.E c = Graph.E c' ∪ {(u1, v1)}" 
                    unfolding Graph.E_def using fct4 fct0 by auto
                  moreover have "u1 ∉ set (pd' a)"
                    proof (rule ccontr)
                      assume "¬ ?thesis"
                      then have "c' (u1, a) ≠ 0" 
                        using fct unfolding Graph.E_def by auto
                      thus "False" using True ‹a = v1› by simp
                    qed
                  ultimately show ?thesis using ‹a = v1› fct by auto
              next
                case False
                  thus ?thesis using fct0 obt3 by auto
              qed
        }
        ultimately have 
          "∀u. set (pred u) = (Graph.E c)¯`` {u} ∧ distinct (pred u)" 
          by metis
      }
      moreover {
        {
          fix a
          assume "a ≠ u1 ∧ a ≠ v1"
          then have "adjmap a = ps' a" using fct8 by simp
            moreover have "set (ps' a) = 
              Graph.E c'``{a} ∪ (Graph.E c')¯``{a} ∧ distinct (ps' a)" 
              using fct by blast
            ultimately have 
              "set (adjmap a) = Graph.E c``{a} ∪ (Graph.E c)¯``{a} 
                ∧ distinct (adjmap a)" 
              unfolding Graph.E_def using fct4 ‹a ≠ u1 ∧ a ≠ v1› by auto
        }
        moreover {
          fix a
          assume "a = u1 ∨ a = v1"
          then have 
            "set (adjmap a) = Graph.E c``{a} ∪ (Graph.E c)¯``{a} 
              ∧ distinct (adjmap a)"
            proof
              assume "a = u1"
              show ?thesis
                proof (cases "c' (u1, v1) = 0 ∧ c' (v1, u1) = 0")
                  case True
                    have fct: 
                      "set (ps' a) = Graph.E c' `` {a} ∪ (Graph.E c')¯ `` {a} 
                      ∧ distinct (ps' a)" 
                      using fct by blast
                    
                    have "adjmap a = v1 # ps' a" 
                      using ‹a = u1› fct8 True by simp
                    moreover have "Graph.E c = Graph.E c' ∪ {(u1, v1)}" 
                      unfolding Graph.E_def using fct4 fct0 by auto
                    moreover have "v1 ∉ set (ps' a)"
                      proof (rule ccontr)
                        assume "¬ ?thesis"
                        then have "c' (a, v1) ≠ 0 ∨ c' (v1, a) ≠ 0"
                          using fct unfolding Graph.E_def by auto
                        thus "False" using True ‹a = u1› by simp
                      qed
                    ultimately show ?thesis using ‹a = u1› fct by auto
                next
                  case False
                    thus ?thesis using fct0 obt3 by auto 
                qed
            next
              assume "a = v1"
              show ?thesis
                proof (cases "c' (u1, v1) = 0 ∧ c' (v1, u1) = 0")
                  case True
                    have fct: 
                      "set (ps' a) = Graph.E c' `` {a} ∪ (Graph.E c')¯ `` {a} 
                      ∧ distinct (ps' a)" 
                      using fct by blast
                    
                    have "adjmap a = u1 # ps' a" 
                      using ‹a = v1› fct8 True by simp
                    moreover have "Graph.E c = Graph.E c' ∪ {(u1, v1)}" 
                      unfolding Graph.E_def using fct4 fct0 by auto
                    moreover have "u1 ∉ set (ps' a)"
                      proof (rule ccontr)
                        assume "¬ ?thesis"
                        then have "c' (u1, a) ≠ 0 ∨ c' (a, u1) ≠ 0"
                          using fct unfolding Graph.E_def by auto
                        thus "False" using True ‹a = v1› by simp
                      qed
                    ultimately show ?thesis using ‹a = v1› fct by auto
                next
                  case False
                    thus ?thesis using fct0 obt3 by auto
                qed
            qed
        }
        ultimately have 
          "∀u. set (adjmap u) = Graph.E c``{u} ∪ (Graph.E c)¯``{u} 
          ∧ distinct (adjmap u)" 
          by metis
      }
      ultimately show ?case by simp  
    qed
    
  lemma read_correct2: "read el s t = None ⟹ ¬ln_invar el 
    ∨ (∃u v c. (u,v,c) ∈ set el ∧ ¬(c > 0))
    ∨ (∃u c. (u, u, c) ∈ set el ∧ c ≠ 0) ∨ 
    (∃u c. (u, s, c) ∈ set el ∧ c ≠ 0) ∨ (∃u c. (t, u, c) ∈ set el ∧ c ≠ 0) ∨
    (∃u v c1 c2. (u, v, c1) ∈ set el ∧ (v, u, c2) ∈ set el ∧ c1 ≠ 0 ∧ c2 ≠ 0)"
    proof (induction el)
      case Nil
        thus ?case by auto
    next
      case (Cons e el)
        thus ?case
          proof (cases "read el s t = None")
            case True
              note Cons.IH[OF this]
              thus ?thesis
                proof
                  assume "¬ln_invar el"
                  then have "¬distinct (map (λ(u, v, _). (u,v)) (e # el)) ∨ 
                    (∃(u, v, c) ∈ set (e # el). ¬(c>0))" 
                    unfolding ln_invar_def by fastforce
                  thus ?thesis unfolding ln_invar_def by fastforce
                next
                  assume "
                    (∃u v c. (u, v, c) ∈ set (el) ∧ ¬(c > 0)) 
                  ∨ (∃u c. (u, u, c) ∈ set el ∧ c ≠ 0) 
                  ∨ (∃u c. (u, s, c) ∈ set el ∧ c ≠ 0) 
                  ∨ (∃u c. (t, u, c) ∈ set el ∧ c ≠ 0) 
                  ∨ (∃u v c1 c2. (u, v, c1) ∈ set el ∧ (v, u, c2) ∈ set el 
                      ∧ c1 ≠ 0 ∧ c2 ≠ 0)" 
                  
                  moreover {
                    assume "(∃u v c. (u, v, c) ∈ set el ∧ ¬(c > 0))"
                    then have "(∃u v c. (u, v, c) ∈ set (e # el) ∧ ¬(c > 0))" 
                      by auto
                  }
                  moreover {
                    assume "(∃u c. (u, u, c) ∈ set el ∧ c ≠ 0)"
                    then have "(∃u c. (u, u, c) ∈ set (e # el) ∧ c ≠ 0)" 
                      by auto
                  }
                  moreover {
                    assume "(∃u c. (u, s, c) ∈ set el ∧ c ≠ 0)"
                    then have "(∃u c. (u, s, c) ∈ set (e # el) ∧ c ≠ 0)" 
                      by auto
                  }
                  moreover {
                    assume "(∃u c. (t, u, c) ∈ set el ∧ c ≠ 0)"
                    then have "(∃u c. (t, u, c) ∈ set (e # el) ∧ c ≠ 0)" 
                      by auto
                  }
                  moreover {
                    assume "(∃u v c1 c2. 
                      (u, v, c1) ∈ set el ∧ (v, u, c2) ∈ set el 
                        ∧ c1 ≠ 0 ∧ c2 ≠ 0)"
                    then have "(∃u v c1 c2. (u, v, c1) ∈ set (e # el) ∧
                      (v, u, c2) ∈ set (e # el) ∧ c1 ≠ 0 ∧ c2 ≠ 0)" 
                      by auto
                  }
                  ultimately show ?thesis by blast
                qed
          next
            case False
            then obtain x where obt1: "read el s t = Some x" by auto
            obtain u1 v1 c1 where obt2: "e = (u1, v1, c1)" 
              apply (cases e) by auto
            obtain c' V' sc' pd' ps' s_n' t_n' where obt3: "x = 
              ⦇
                pn_c = c', pn_V = V', pn_succ = sc',
                pn_pred = pd', pn_adjmap = ps',
                pn_s_node = s_n', pn_t_node = t_n'
              ⦈" 
              apply (cases x) by auto 
            then have "(el, c') ∈ ln_rel" using obt1 read_correct1[of el s t] 
              by simp
            then have "c' = ln_α el" unfolding ln_rel_def br_def by simp
            

            have "(c' (u1, v1) ≠ 0 ∨ c' (v1, u1) ≠ 0 ∨ c1 ≤ 0) ∨ 
              (c1 > 0 ∧ (u1 = v1 ∨ v1 = s ∨ u1 = t))"
              using obt1 obt2 obt3 False Cons.prems 
                by (auto split:option.splits if_splits)
            moreover {
              assume "c1 ≤ 0"
              then have "¬ ln_invar (e # el)" 
                unfolding ln_invar_def using obt2 by auto
            }
            moreover {
              assume "c1 > 0 ∧ u1 = v1"
              then have "(∃u c. (u, u, c) ∈ set (e # el) ∧ c > 0)" 
                using obt2 by auto
            }
            moreover {
              assume "c1 > 0 ∧ v1 = s"
              then have "(∃u c. (u, s, c) ∈ set (e # el) ∧ c > 0)" 
                using obt2 by auto
            }
            moreover {
              assume "c1 > 0 ∧ u1 = t"
              then have "(∃u c. (t, u, c) ∈ set (e # el) ∧ c > 0)" 
                using obt2 by auto
            }
            moreover {
              assume "c' (u1, v1) ≠ 0"
              then have "∃c1'. (u1, v1, c1') ∈ set el" 
                using ‹c' = ln_α el› unfolding ln_α_def 
                by (auto split:if_splits)
              then have "¬ distinct (map (λ(u, v, _). (u, v)) (e # el))" 
                using obt2 by force
              then have "¬ln_invar (e # el)" unfolding ln_invar_def by auto
            }
            moreover {
              assume "c' (v1, u1) ≠ 0"
              then have "∃c1'. (v1, u1, c1') ∈ set el ∧ c1' ≠ 0" 
                using ‹c' = ln_α el› unfolding ln_α_def 
                by (auto split:if_splits)
              then have "¬ln_invar (e # el) ∨ (
                ∃u v c1 c2.
                  (u, v, c1) ∈ set (e # el) ∧ (v, u, c2) ∈ set (e # el) 
                  ∧ c1 ≠ 0 ∧ c2 ≠ 0)"
                proof (cases "c1 ≠ 0")
                  case True
                    thus ?thesis 
                      using ‹∃c1'. (v1, u1, c1') ∈ set el  ∧ c1' ≠ 0› obt2 
                      by auto
                next
                  case False
                    then have "¬ln_invar (e # el)" 
                      unfolding ln_invar_def using obt2 by auto
                    thus ?thesis by blast
                qed
            }
            ultimately show ?thesis by blast
          qed
    qed
    
  subsection ‹Implementation of Pre-Networks›  

  record 'capacity::linordered_idom pre_network' =
    pn_c' :: "(nat*nat,'capacity) ArrayHashMap.ahm"
    pn_V' :: "nat ahs"
    pn_succ' :: "(nat,nat list) ArrayHashMap.ahm"
    pn_pred' :: "(nat,nat list) ArrayHashMap.ahm"
    pn_adjmap' :: "(nat,nat list) ArrayHashMap.ahm"
    pn_s_node' :: bool
    pn_t_node' :: bool


  definition "pnet_α pn' ≡ ⦇
      pn_c = the_default 0 o (ahm.α (pn_c' pn')), 
      pn_V = ahs_α (pn_V' pn'), 
      pn_succ = the_default [] o (ahm.α (pn_succ' pn')),
      pn_pred = the_default [] o (ahm.α (pn_pred' pn')),
      pn_adjmap = the_default [] o (ahm.α (pn_adjmap' pn')), 
      pn_s_node = pn_s_node' pn', 
      pn_t_node = pn_t_node' pn'
  ⦈"  

  definition "pnet_rel ≡ br pnet_α (λ_. True)"
  
  definition "ahm_ld a ahm k ≡ the_default a (ahm.lookup k ahm)"
  abbreviation "cap_lookup ≡ ahm_ld 0"
  abbreviation "succ_lookup ≡ ahm_ld []"


  fun read' :: "(nat × nat × 'capacity::linordered_idom) list ⇒ nat ⇒ nat ⇒
    'capacity pre_network' option" where
    "read' [] _ _ = Some ⦇
      pn_c' = ahm.empty (), 
      pn_V' = ahs.empty (), 
      pn_succ' = ahm.empty (),
      pn_pred' = ahm.empty (),
      pn_adjmap' = ahm.empty (), 
      pn_s_node' = False, 
      pn_t_node' = False
    ⦈"
  | "read' ((u, v, c) # es) s t = ((case (read' es s t) of 
      Some x ⇒
        (if 
          cap_lookup (pn_c' x) (u, v) = 0 
          ∧ cap_lookup (pn_c' x) (v, u) = 0 ∧ c > 0 
         then
          (if u = v ∨ v = s ∨ u = t then
            None
          else
            Some (x⦇ 
              pn_c' := ahm.update (u, v) c (pn_c' x),
              pn_V' := ahs.ins u (ahs.ins v (pn_V' x)),
              pn_succ' := 
                ahm.update u (v # (succ_lookup (pn_succ' x) u)) (pn_succ' x),
              pn_pred' := 
                ahm.update v (u # (succ_lookup (pn_pred' x) v)) (pn_pred' x),
              pn_adjmap' := ahm.update 
                u (v # (succ_lookup (pn_adjmap' x) u)) (ahm.update 
                v (u # (succ_lookup (pn_adjmap' x) v)) 
                (pn_adjmap' x)),
              pn_s_node' := pn_s_node' x ∨ u = s,
              pn_t_node' := pn_t_node' x ∨ v = t
            ⦈))
        else
          None)
    | None ⇒ None))"

  lemma read'_correct: "read el s t = map_option pnet_α (read' el s t)"
    apply (induction el s t rule: read.induct)
    by (auto 
      simp: pnet_α_def o_def ahm.correct ahs.correct ahm_ld_def 
      split: option.splits) (* Takes long *)
    
  lemma read'_correct_alt: "(read' el s t, read el s t) ∈ ⟨pnet_rel⟩option_rel"
    unfolding pnet_rel_def br_def
    apply (simp add: option_rel_def read'_correct)
    using domIff by force

  export_code read checking SML     
  
  subsection ‹Usefulness Check›
  text ‹
    We have to check that every node in the network is useful,
    i.e., lays on a path from source to sink.
    ›

  definition "reachable_spec c s ≡ RETURN (((Graph.E c)⇧*)``{s}) "
  definition "reaching_spec c t ≡ RETURN ((((Graph.E c)¯)⇧*)``{t})"

  definition "checkNet cc s t ≡ do {
    if s = t then
      RETURN None
    else do {
      let rd = read cc s t;
      case rd of 
        None ⇒ RETURN None
      | Some x ⇒ do {                
          if pn_s_node x ∧ pn_t_node x then
            do {
              ASSERT(finite ((Graph.E (pn_c x))⇧* `` {s}));
              ASSERT(finite (((Graph.E (pn_c x))¯)⇧* `` {t}));
              ASSERT(∀u. set ((pn_succ x) u) = Graph.E (pn_c x) `` {u} 
                ∧ distinct ((pn_succ x) u));
              ASSERT(∀u. set ((pn_pred x) u) = (Graph.E (pn_c x))¯ `` {u}   
                ∧ distinct ((pn_pred x) u));
              
              succ_s ← reachable_spec (pn_c x) s;
              pred_t ← reaching_spec (pn_c x) t;
              if (pn_V x) = succ_s ∧ (pn_V x) = pred_t then
                RETURN (Some (pn_c x, pn_adjmap x))
              else
                RETURN None
            }
          else
            RETURN None
        }
      }
    }"

  lemma checkNet_pre_correct1 : "checkNet el s t ≤ 
    SPEC (λ r. r = Some (c, adjmap) ⟶ (el, c) ∈ ln_rel ∧ Network c s t ∧ 
    (∀u. set (adjmap u) = Graph.E c``{u} ∪ (Graph.E c)¯``{u} 
      ∧ distinct (adjmap u)))"
    unfolding checkNet_def reachable_spec_def reaching_spec_def
    apply (refine_vcg)
    apply clarsimp_all
      proof -
        {
          fix x
          assume asm1: "s ≠ t"
          assume asm2: "read el s t = Some x"
          assume asm3: "pn_s_node x"
          assume asm4: "pn_t_node x"
          obtain c V sc pd adjmap  where obt: "x = 
            ⦇
              pn_c = c, pn_V = V,
              pn_succ = sc, pn_pred = pd,  pn_adjmap = adjmap, 
              pn_s_node = True, pn_t_node = True
            ⦈"
            apply (cases x) using asm3 asm4 by auto
          then have "read el s t = Some ⦇
            pn_c = c, pn_V = V, pn_succ = sc, pn_pred = pd, 
            pn_adjmap = adjmap, pn_s_node = True, pn_t_node = True⦈" 
            using asm2 by simp
          note fct = read_correct1[OF this]
          
          then have [simp, intro!]: "finite (Graph.V c)" by blast
          have "Graph.E c ⊆ (Graph.V c) × (Graph.V c)" 
            unfolding Graph.V_def by auto
          from finite_subset[OF this] have "finite (Graph.E (pn_c x))" 
            by (simp add: obt)
          then show "finite ((Graph.E (pn_c x))⇧* `` {s})" 
            and "finite (((Graph.E (pn_c x))¯)⇧* `` {t})"  
            by (auto simp add: finite_rtrancl_Image)
        }
        {
          fix x
          assume asm1: "s ≠ t"
          assume asm2: "read el s t = Some x"
          assume asm3: "finite ((Graph.E (pn_c x))⇧* `` {s})"
          assume asm4: "finite (((Graph.E (pn_c x))¯)⇧* `` {t})"
          assume asm5: "pn_s_node x"
          assume asm6: "pn_t_node x" 
          obtain c V sc pd adjmap  where obt: "x = ⦇pn_c = c, pn_V = V,
            pn_succ = sc, pn_pred = pd,  pn_adjmap = adjmap, 
            pn_s_node = True, pn_t_node = True⦈"
            apply (cases x) using asm5 asm6 by auto
          then have "read el s t = Some ⦇pn_c = c, pn_V = V, 
            pn_succ = sc, pn_pred = pd, pn_adjmap = adjmap, 
            pn_s_node = True, pn_t_node = True⦈" 
            using asm2 by simp
          note fct = read_correct1[OF this]
          
          have "⋀u. set ((pn_succ x) u) 
            = Graph.E (pn_c x) `` {u} ∧ distinct ((pn_succ x) u)"
            using fct obt by simp
          moreover have "⋀u. set ((pn_pred x) u) = (Graph.E (pn_c x))¯ `` {u} ∧ 
            distinct ((pn_pred x) u)" using fct obt by simp
          ultimately show "⋀u. set ((pn_succ x) u) = Graph.E (pn_c x) `` {u}" 
            and "⋀u. distinct ((pn_succ x) u)" 
            and "⋀u. set ((pn_pred x) u) = (Graph.E (pn_c x))¯ `` {u}"
            and "⋀u.  distinct ((pn_pred x) u)" 
            by auto 
        }
        {
          fix x
          assume asm1: "s ≠ t"
          assume asm2: "read el s t = Some x"
          assume asm3: "pn_s_node x"
          assume asm4: "pn_t_node x"
          assume asm5: 
            "((Graph.E (pn_c x))¯)⇧* `` {t} = (Graph.E (pn_c x))⇧* `` {s}"
          assume asm6: "pn_V x = (Graph.E (pn_c x))⇧* `` {s}" 
          assume asm7: "c = pn_c x"
          assume asm8: "adjmap = pn_adjmap x"
          obtain V sc pd  where obt: "x = ⦇pn_c = c, pn_V = V,
            pn_succ = sc, pn_pred = pd,  pn_adjmap = adjmap, 
            pn_s_node = True, pn_t_node = True⦈"
            apply (cases x) using asm3 asm4 asm7 asm8 by auto
          then have "read el s t = Some ⦇pn_c = c, pn_V = V, 
            pn_succ = sc, pn_pred = pd, pn_adjmap = adjmap, 
            pn_s_node = True, pn_t_node = True⦈" 
            using asm2 by simp
          note fct = read_correct1[OF this]
          
          have "⋀u. set ((pn_succ x) u) = Graph.E (pn_c x) `` {u} 
            ∧ distinct ((pn_succ x) u)"
            using fct obt by simp
          moreover have "⋀u. set ((pn_pred x) u) = (Graph.E (pn_c x))¯ `` {u} ∧ 
            distinct ((pn_pred x) u)" using fct obt by simp
          moreover have "(el, pn_c x) ∈ ln_rel" using fct asm7 by simp
          moreover {
            {
              {
                have "Graph.V c ⊆ ((Graph.E c))⇧* `` {s}" 
                  using asm6 obt fct by simp
                then have "∀v∈(Graph.V c). Graph.isReachable c s v" 
                  unfolding Graph.connected_def using Graph.rtc_isPath[of s _ c] 
                  by auto
              }
              moreover {
                have "Graph.V c ⊆ ((Graph.E c)¯)⇧* `` {t}" 
                  using asm5 asm6 obt fct by simp
                then have "∀v∈(Graph.V c). Graph.isReachable c v t"
                  unfolding Graph.connected_def using Graph.rtci_isPath 
                  by fastforce
              }
              ultimately have 
                "∀v∈(Graph.V c). Graph.isReachable c s v 
                ∧ Graph.isReachable c v t" 
                by simp
            }
            moreover {
              have "finite (Graph.V c)" and "s ∈ (Graph.V c)" 
                using fct obt by auto
              note Graph.reachable_ss_V[OF ‹s ∈ (Graph.V c)›]
              note finite_subset[OF this ‹finite (Graph.V c)›]
            }
            ultimately have "Network (pn_c x) s t" 
              unfolding Network_def using asm1 fct asm7 
              by (simp add: Graph.E_def)
          }
          moreover have "∀u.(set (pn_adjmap x u) =
            Graph.E (pn_c x) `` {u} ∪ (Graph.E (pn_c x))¯ `` {u})" 
            using fct obt by simp
          moreover have "∀u. distinct (pn_adjmap x u)" using fct obt by simp
          ultimately show "(el, pn_c x) ∈ ln_rel" and "Network (pn_c x) s t" and
            "⋀u. set (pn_adjmap x u) 
              = Graph.E (pn_c x) `` {u} ∪ (Graph.E (pn_c x))¯ `` {u}" 
            and "⋀u. distinct (pn_adjmap x u)" by auto
        }
      qed
  
  lemma checkNet_pre_correct2_aux: 
    assumes asm1: "s ≠ t"
    assumes asm2: "read el s t = Some x" 
    assumes asm3: 
      "∀u. set (pn_succ x u) = Graph.E (pn_c x) `` {u} ∧ distinct (pn_succ x u)"
    assumes asm4: "∀u. set (pn_pred x u) = (Graph.E (pn_c x))¯ `` {u} 
      ∧ distinct (pn_pred x u)"
    assumes asm5: "pn_V x = (Graph.E (pn_c x))⇧* `` {s} 
      ⟶ (Graph.E (pn_c x))⇧* `` {s} ≠ ((Graph.E (pn_c x))¯)⇧* `` {t}"
    assumes asm6: "pn_s_node x"
    assumes asm7: "pn_t_node x"
    assumes asm8: "ln_invar el"
    assumes asm9: "Network (ln_α el) s t"
    shows "False"
    proof -          
      obtain c V sc pd ps  where obt: "x = ⦇pn_c = c, pn_V = V, 
        pn_succ = sc, pn_pred = pd, pn_adjmap = ps, 
        pn_s_node = True, pn_t_node = True⦈"
        apply (cases x) using asm3 asm4 asm6 asm7 by auto
      then have "read el s t = Some ⦇pn_c = c, pn_V = V, 
        pn_succ = sc, pn_pred = pd, pn_adjmap = ps, 
        pn_s_node = True, pn_t_node = True⦈" 
        using asm2 by simp
      note fct = read_correct1[OF this]
      
      have "pn_V x ≠ (Graph.E (pn_c x))⇧* `` {s} 
        ∨ (pn_V x = (Graph.E (pn_c x))⇧* `` {s} 
            ∧ ((Graph.E (pn_c x))¯)⇧* `` {t} ≠ (Graph.E (pn_c x))⇧* `` {s})" 
        using asm5 by blast
      thus "False"
        proof
          assume "pn_V x = (Graph.E (pn_c x))⇧* `` {s} ∧ 
            ((Graph.E (pn_c x))¯)⇧* `` {t} ≠ (Graph.E (pn_c x))⇧* `` {s}"
          then have "¬(Graph.V c ⊆ ((Graph.E c)¯)⇧* `` {t}) 
            ∨ ¬(((Graph.E c)¯)⇧* `` {t} ⊆ Graph.V c)"
            using asm5  obt fct by simp
          then have "∃v∈(Graph.V c). ¬Graph.isReachable c v t"
            proof
              assume "¬(((Graph.E c)¯)⇧* `` {t} ⊆ Graph.V c)"
              then obtain x where 
                o1: "x ∈ ((Graph.E c)¯)⇧* `` {t} ∧ x ∉ Graph.V c" 
                by blast
              then have "∃p. Graph.isPath c x p t" 
                using Graph.rtci_isPath by auto
              then obtain p where "Graph.isPath c x p t" by blast
              then have "x ∈ Graph.V c"
                proof (cases "p = []")
                  case True
                    then have "x = t" 
                      using ‹Graph.isPath c x p t› Graph.isPath.simps(1) 
                      by auto
                    thus ?thesis using fct by auto
                next
                  case False
                    then obtain p1 ps where "p = p1 # ps" 
                      by (meson neq_Nil_conv)
                    then have "Graph.isPath c x (p1 # ps) t" 
                      using ‹Graph.isPath c x p t› by auto
                    then have "fst p1 = x ∧ c p1 ≠ 0" 
                      using Graph.isPath_head[of c x p1 ps t] 
                      by (auto simp: Graph.E_def)
                    then have "∃v. c (x, v) ≠ 0" by (metis prod.collapse)
                    then have "x ∈ Graph.V c" 
                      unfolding Graph.V_def Graph.E_def by auto
                    thus ?thesis by simp
                qed
              thus ?thesis using o1 by auto
            next
              assume "¬(Graph.V c ⊆ ((Graph.E c)¯)⇧* `` {t})"
              then obtain x where 
                o1: "x ∉ ((Graph.E c)¯)⇧* `` {t} ∧ x ∈ Graph.V c" 
                by blast
              then have "(x , t) ∉ (Graph.E c)⇧*" 
                by (meson Image_singleton_iff rtrancl_converseI)
              have "∀p. ¬Graph.isPath c x p t"
                proof (rule ccontr)
                  assume "¬?thesis"
                  then obtain p where "Graph.isPath c x p t" by blast
                  thus "False" using Graph.isPath_rtc ‹(x , t) ∉ (Graph.E c)⇧*› 
                  by auto
                qed
              then have "¬Graph.isReachable c x t" 
                unfolding Graph.connected_def by auto
              thus ?thesis using o1 by auto
            qed
          moreover {
            have "(el, c) ∈ ln_rel" using fct obt by simp
            then have "c = ln_α el" unfolding ln_rel_def br_def by auto
          }
          ultimately have "¬Network (ln_α el) s t" 
            unfolding Network_def by auto
          thus ?thesis using asm9 by blast
        next
          assume "pn_V x ≠ (Graph.E (pn_c x))⇧* `` {s}"
          
          then have "¬(Graph.V c ⊆ (Graph.E c)⇧* `` {s}) 
            ∨ ¬((Graph.E c)⇧* `` {s} ⊆ Graph.V c)"
            using asm5  obt fct by simp
          then have "∃v∈(Graph.V c). ¬Graph.isReachable c s v"
            proof
              assume "¬((Graph.E c)⇧* `` {s} ⊆ Graph.V c)"
              then obtain x where o1:"x ∈ (Graph.E c)⇧* `` {s} ∧ x ∉ Graph.V c" 
                by blast
              then have "∃p. Graph.isPath c s p x" 
                using Graph.rtc_isPath by auto
              then obtain p where "Graph.isPath c s p x" by blast
              then have "x ∈ Graph.V c"
                proof (cases "p = []")
                  case True
                    then have "x = s" 
                      using ‹Graph.isPath c s p x› 
                      by (auto simp: Graph.isPath.simps(1))
                    thus ?thesis using fct by auto
                next
                  case False
                    then obtain p1 ps where "p = ps @ [p1]" 
                      by (metis append_butlast_last_id)
                    then have "Graph.isPath c s (ps @ [p1]) x"
                      using ‹Graph.isPath c s p x› by auto
                    then have "snd p1 = x ∧ c p1 ≠ 0"
                      using Graph.isPath_tail[of c s ps p1 x] 
                      by (auto simp: Graph.E_def)
                    then have "∃v. c (v, x) ≠ 0" by (metis prod.collapse)
                    then have "x ∈ Graph.V c" 
                      unfolding Graph.V_def Graph.E_def by auto
                    thus ?thesis by simp
                qed
              thus ?thesis using o1 by auto
            next
              assume "¬(Graph.V c ⊆ (Graph.E c)⇧* `` {s})"
              then obtain x where o1: "x ∉ (Graph.E c)⇧* `` {s} ∧ x ∈ Graph.V c" 
                by blast
              then have "(s , x) ∉ (Graph.E c)⇧*" 
                by (meson Image_singleton_iff rtrancl_converseI)
              have "∀p. ¬Graph.isPath c s p x"
                proof (rule ccontr)
                  assume "¬?thesis"
                  then obtain p where "Graph.isPath c s p x" by blast
                  thus "False" using Graph.isPath_rtc ‹(s, x) ∉ (Graph.E c)⇧*› 
                    by auto
                qed
              then have "¬Graph.isReachable c s x" 
                unfolding Graph.connected_def by auto
              thus ?thesis using o1 by auto
            qed
          moreover {
            have "(el, c) ∈ ln_rel" using fct obt by simp
            then have "c = ln_α el" unfolding ln_rel_def br_def by auto
          }
          ultimately have "¬Network (ln_α el) s t" 
            unfolding Network_def by auto
          thus ?thesis using asm9 by blast
        qed
    qed

  lemma checkNet_pre_correct2:
    "checkNet el s t 
    ≤ SPEC (λr. r = None ⟶ ¬ln_invar el ∨ ¬Network (ln_α el) s t)"
    unfolding checkNet_def reachable_spec_def reaching_spec_def
    apply (refine_vcg)
    apply (clarsimp_all) 
    proof -
      {
        assume "s = t" and "ln_invar el" and "Network (ln_α el) t t"
        thus "False" using Network_def by auto
      }
      next {
        assume "s ≠ t" and "read el s t = None" and "ln_invar el" 
          and "Network (ln_α el) s t"
        note read_correct2[OF ‹read el s t = None›]
        thus "False"
          proof
            assume "¬ln_invar el"
            thus ?thesis using ‹ln_invar el› by blast
          next
            assume asm: "
              (∃u v c. (u, v, c) ∈ set el ∧ ¬(c > 0)) 
            ∨ (∃u c. (u, u, c) ∈ set el ∧ c≠0) 
            ∨ (∃u c. (u, s, c) ∈ set el ∧ c≠0) 
            ∨ (∃u c. (t, u, c) ∈ set el ∧ c≠0) 
            ∨ (∃u v c1 c2. (u, v, c1) ∈ set el 
                ∧ (v, u, c2) ∈ set el ∧ c1≠0 ∧ c2≠0)"
            
            moreover {
              assume A: "(∃u v c. (u, v, c) ∈ set el ∧ ¬(c>0))"
              then have "¬ln_invar el" 
                using not_less by (fastforce simp: ln_invar_def)
              with ‹ln_invar el› have False by simp
            }
            moreover {
              assume "(∃u c. (u, u, c) ∈ set el ∧ c≠0)"
              then have "∃ u. ln_α el (u, u) ≠ 0" 
                unfolding ln_α_def apply (auto split:if_splits)
                by (metis (mono_tags, lifting) tfl_some)
              then have "False" 
                using ‹Network (ln_α el) s t› 
                unfolding Network_def by (auto simp: Graph.E_def)
            }
            moreover {
              assume "(∃u c. (u, s, c) ∈ set el ∧ c≠0)"
              then have "∃ u. ln_α el (u, s) ≠ 0" 
                unfolding ln_α_def 
                by (clarsimp) (metis (mono_tags, lifting) tfl_some)
              then have "False" 
                using ‹Network (ln_α el) s t› unfolding Network_def 
                by (auto simp: Graph.E_def)
            }
            moreover {
              assume "(∃u c. (t, u, c) ∈ set el ∧ c≠0)"
              then have "∃ u. ln_α el (t, u) ≠ 0" 
              unfolding ln_α_def 
                by (clarsimp) (metis (mono_tags, lifting) tfl_some)
              then have "False" 
                using ‹Network (ln_α el) s t› unfolding Network_def 
                by (auto simp: Graph.E_def)
            }
            moreover {
              assume "(∃u v c1 c2. 
                (u, v, c1) ∈ set el ∧ (v, u, c2) ∈ set el ∧ c1≠0 ∧ c2≠0)"
              then obtain u v c1 c2 where 
                o1: "(u, v, c1) ∈ set el ∧ (v, u, c2) ∈ set el 
                    ∧ c1≠0 ∧ c2≠0" 
                by blast
              then have "ln_α el (u, v) ≠ 0" unfolding ln_α_def
                by (clarsimp) (metis (mono_tags, lifting) tfl_some)
              moreover have "ln_α el (v, u) ≠ 0" unfolding ln_α_def using o1 
                by (clarsimp) (metis (mono_tags, lifting) tfl_some)
              ultimately have 
                "¬ (∀u v. (ln_α el) (u, v) ≠ 0 ⟶ (ln_α el) (v, u) = 0)" 
                by auto
              then have "False" 
                using ‹Network (ln_α el) s t› unfolding Network_def 
                by (auto simp: Graph.E_def)
            }
            ultimately show ?thesis by force
          qed
      }
      next {
        fix x
        assume asm1: "s ≠ t"
        assume asm2: "read el s t = Some x"
        assume asm3: "pn_s_node x"
        assume asm4: "pn_t_node x"
        obtain c V sc pd adjmap  where obt: "x = ⦇pn_c = c, pn_V = V,
          pn_succ = sc, pn_pred = pd,  pn_adjmap = adjmap, 
          pn_s_node = True, pn_t_node = True⦈"
          apply (cases x) using asm3 asm4 by auto
        then have "read el s t = Some ⦇pn_c = c, pn_V = V, 
          pn_succ = sc, pn_pred = pd, pn_adjmap = adjmap, 
          pn_s_node = True, pn_t_node = True⦈" 
          using asm2 by simp
        note fct = read_correct1[OF this]
        
        then have [simp]: "finite (Graph.V c)" by blast
        have "Graph.E c ⊆ (Graph.V c) × (Graph.V c)" 
          unfolding Graph.V_def by auto
        from finite_subset[OF this] have "finite (Graph.E (pn_c x))" 
          by (auto simp: obt)
        then show  "finite ((Graph.E (pn_c x))⇧* `` {s})" 
          and "finite (((Graph.E (pn_c x))¯)⇧* `` {t})"  
          by (auto simp add: finite_rtrancl_Image)
      }
      {
        fix x
        assume asm1: "s ≠ t"
        assume asm2: "read el s t = Some x"
        assume asm3: "finite ((Graph.E (pn_c x))⇧* `` {s})"
        assume asm4: "finite (((Graph.E (pn_c x))¯)⇧* `` {t})"
        assume asm5: "pn_s_node x"
        assume asm6: "pn_t_node x" 
        obtain c V sc pd adjmap  where obt: "x = ⦇pn_c = c, pn_V = V,
          pn_succ = sc, pn_pred = pd, pn_adjmap = adjmap, 
          pn_s_node = True, pn_t_node = True⦈"
          apply (cases x) using asm5 asm6 by auto
        then have "read el s t = Some ⦇pn_c = c, pn_V = V, pn_succ = sc, 
          pn_pred = pd, pn_adjmap = adjmap, pn_s_node = True, pn_t_node = True⦈" 
          using asm2 by simp
        note fct = read_correct1[OF this]
        
        have "⋀u. set ((pn_succ x) u) = Graph.E (pn_c x) `` {u} 
          ∧ distinct ((pn_succ x) u)"
          using fct obt by simp
        moreover have "⋀u. set ((pn_pred x) u) = (Graph.E (pn_c x))¯ `` {u} ∧ 
          distinct ((pn_pred x) u)" 
          using fct obt by simp
        ultimately show  "⋀u. set ((pn_succ x) u) = Graph.E (pn_c x) `` {u}" 
          and "⋀u. distinct ((pn_succ x) u)" 
          and "⋀u. set ((pn_pred x) u) = (Graph.E (pn_c x))¯ `` {u}"
          and "⋀u.  distinct ((pn_pred x) u)" 
          by auto 
      }
      next {
        fix x
        assume asm1: "s ≠ t"
        assume asm2: "read el s t = Some x"
        assume asm3: "pn_s_node x ⟶ ¬pn_t_node x"
        assume asm4: "ln_invar el"
        assume asm5: "Network (ln_α el) s t"
        obtain c V sc pd ps s_node t_node where 
          obt: "x = ⦇pn_c = c, pn_V = V, pn_succ = sc, pn_pred = pd, 
          pn_adjmap = ps, pn_s_node = s_node, pn_t_node = t_node⦈" 
          by (cases x) 
        then have "read el s t = Some ⦇pn_c = c, pn_V = V, pn_succ = sc, 
          pn_pred = pd, pn_adjmap = ps, pn_s_node = s_node, pn_t_node = t_node⦈" 
          using asm2 by simp
        note fct = read_correct1[OF this]
        
        have "(el, c) ∈ ln_rel" using fct obt by simp
        then have "c = ln_α el" unfolding ln_rel_def br_def by auto
        
        have "¬pn_s_node x ∨ ¬pn_t_node x" using asm3 by auto 
        then show "False"
          proof
            assume "¬pn_s_node x"
            then have "¬s_node" using obt fct by auto
            then have "s ∉ Graph.V c" using fct by auto
            thus ?thesis using ‹c = ln_α el› asm5 Network_def by auto
          next
            assume "¬pn_t_node x"
            then have "¬t_node" using obt fct by auto
            then have "t ∉ Graph.V c" using fct by auto
            thus ?thesis using ‹c = ln_α el› asm5 Network_def by auto
          qed
      }
    qed (blast dest: checkNet_pre_correct2_aux)  

  lemma checkNet_correct' : "checkNet el s t ≤ SPEC (λ r. case r of 
      Some (c, adjmap) ⇒
        (el, c) ∈ ln_rel ∧ Network c s t 
        ∧ (∀u. set (adjmap u) = Graph.E c``{u} ∪ (Graph.E c)¯``{u} 
           ∧ distinct (adjmap u))
    | None ⇒ ¬ln_invar el ∨ ¬Network (ln_α el) s t)"
    using checkNet_pre_correct1[of el s t] checkNet_pre_correct2[of el s t]
    by (auto split: option.splits simp: pw_le_iff refine_pw_simps)

  lemma checkNet_correct : "checkNet el s t ≤ SPEC (λr. case r of 
      Some (c, adjmap) ⇒ (el, c) ∈ ln_rel ∧ Network c s t 
        ∧ Graph.is_adj_map c adjmap
    | None ⇒ ¬ln_invar el ∨ ¬Network (ln_α el) s t)"
    using checkNet_pre_correct1[of el s t] checkNet_pre_correct2[of el s t]
    by (auto 
        split: option.splits 
        simp: Graph.is_adj_map_def pw_le_iff refine_pw_simps)

  subsection ‹Implementation of Usefulness Check›  
  text ‹We use the DFS framework to implement the usefulness check.
    We have to convert between our graph representation and the CAVA automata 
    library's graph representation used by the DFS framework.
    ›

  definition "graph_of pn s ≡ ⦇
    g_V = UNIV,
    g_E = Graph.E (pn_c pn),
    g_V0 = {s}
  ⦈"

  definition "rev_graph_of pn s ≡ ⦇
    g_V = UNIV,
    g_E = (Graph.E (pn_c pn))¯,
    g_V0 = {s}
  ⦈"

  
  definition "checkNet2 cc s t ≡ do {
    if s = t then
      RETURN None
    else do {
      let rd = read cc s t;
      case rd of 
        None ⇒ RETURN None
      | Some x ⇒ do {                
          if pn_s_node x ∧ pn_t_node x then
            do {
              ASSERT(finite ((Graph.E (pn_c x))⇧* `` {s}));
              ASSERT(finite (((Graph.E (pn_c x))¯)⇧* `` {t}));
              ASSERT(∀u. set ((pn_succ x) u) = Graph.E (pn_c x) `` {u} 
                ∧ distinct ((pn_succ x) u));
              ASSERT(∀u. set ((pn_pred x) u) = (Graph.E (pn_c x))¯ `` {u} 
                ∧ distinct ((pn_pred x) u));
              
              let succ_s = (op_reachable (graph_of x s));
              let pred_t = (op_reachable (rev_graph_of x t));
              if (pn_V x) = succ_s ∧ (pn_V x) = pred_t then
                RETURN (Some (pn_c x, pn_adjmap x))
              else
                RETURN None
            }
          else
            RETURN None
        }
      }
    }"
    
  lemma checkNet2_correct: "checkNet2 c s t ≤ checkNet c s t"
    apply (rule refine_IdD)
    unfolding checkNet_def checkNet2_def graph_of_def rev_graph_of_def 
      reachable_spec_def reaching_spec_def
    apply (refine_rcg)
    apply refine_dref_type
    apply auto
    done
    
  definition "graph_of_impl pn' s ≡ ⦇
    gi_V = λ_. True,
    gi_E = succ_lookup (pn_succ' pn'),
    gi_V0 = [s]
  ⦈"

  definition "rev_graph_of_impl pn' t ≡ ⦇
    gi_V = λ_. True,
    gi_E = succ_lookup (pn_pred' pn'),
    gi_V0 = [t]
  ⦈"
    
  definition "well_formed_pn x ≡ 
    (∀u. set ((pn_succ x) u) = Graph.E (pn_c x) `` {u} 
      ∧ distinct ((pn_succ x) u))"
  
  definition "rev_well_formed_pn x ≡ 
    (∀u. set ((pn_pred x) u) = (Graph.E (pn_c x))¯ `` {u} 
      ∧ distinct ((pn_pred x) u))"
    
  lemma id_slg_rel_alt_a: "⟨Id⟩slg_rel 
    = { (s,E). ∀u. distinct (s u) ∧ set (s u) = E``{u} }"
    by (auto simp add: slg_rel_def br_def list_set_rel_def dest: fun_relD)  
    
  lemma graph_of_impl_correct: "well_formed_pn pn ⟹ (pn', pn) ∈ pnet_rel ⟹
    (graph_of_impl pn' s, graph_of pn s) ∈ ⟨unit_rel,Id⟩g_impl_rel_ext"
    unfolding pnet_rel_def graph_of_impl_def graph_of_def
      g_impl_rel_ext_def gen_g_impl_rel_ext_def
    apply (auto simp: fun_set_rel_def br_def list_set_rel_def 
        id_slg_rel_alt_a ahm_ld_def)
    apply (auto simp: well_formed_pn_def Graph.E_def 
        pnet_α_def o_def ahm_correct)
    done
    
  lemma rev_graph_of_impl_correct:"⟦rev_well_formed_pn pn; (pn',pn)∈pnet_rel⟧ 
    ⟹ 
    (rev_graph_of_impl pn' s, rev_graph_of pn s) ∈ ⟨unit_rel,Id⟩g_impl_rel_ext"
    unfolding pnet_rel_def rev_graph_of_impl_def rev_graph_of_def
      g_impl_rel_ext_def gen_g_impl_rel_ext_def
    apply (auto simp: fun_set_rel_def br_def list_set_rel_def 
        id_slg_rel_alt_a ahm_ld_def)
    apply (auto simp: rev_well_formed_pn_def Graph.E_def pnet_α_def 
        o_def ahm_correct)
    done   
  
  schematic_goal reachable_impl:
    assumes [simp]: "finite ((g_E G)⇧* `` g_V0 G)" "graph G"
    assumes [autoref_rules]: "(Gi,G)∈⟨unit_rel,nat_rel⟩g_impl_rel_ext"
    shows "RETURN (?c::?'c) ≤ ⇓?R (RETURN (op_reachable G))"  
    by autoref_monadic
  concrete_definition reachable_impl uses reachable_impl
  thm reachable_impl.refine

  context begin
    interpretation autoref_syn .

    schematic_goal sets_eq_impl:
      fixes a b :: "nat set"
      assumes [autoref_rules]: "(ai,a) ∈ ⟨nat_rel⟩ahs.rel"
      assumes [autoref_rules]: "(bi,b) ∈ ⟨nat_rel⟩dflt_ahs_rel"
      shows "(?c, (a ::: ⟨nat_rel⟩ahs.rel) = (b ::: ⟨nat_rel⟩dflt_ahs_rel )) 
        ∈ bool_rel"
      apply (autoref)
      done
    concrete_definition sets_eq_impl uses sets_eq_impl  

  end
  
  definition "net_α ≡ (λ(ci, adjmapi) . 
    ((the_default 0 o (ahm.α ci)), (the_default [] o (ahm.α adjmapi))))"

  lemma [code]: "net_α (ci, adjmapi) = (
    cap_lookup ci, succ_lookup adjmapi
    )"
    unfolding net_α_def 
    by (auto split: option.splits simp: ahm.correct ahm_ld_def)

  definition "checkNet3 cc s t ≡ do {
    if s = t then
      RETURN None
    else do {
      let rd = read' cc s t;
      case rd of 
        None ⇒ RETURN None
      | Some x ⇒ do {                
          if pn_s_node' x ∧ pn_t_node' x then
            do {
              ASSERT(finite ((Graph.E (pn_c (pnet_α x)))⇧* `` {s}));
              ASSERT(finite (((Graph.E (pn_c (pnet_α x)))¯)⇧* `` {t}));
              ASSERT(∀u. set ((pn_succ (pnet_α x)) u) =
                Graph.E (pn_c (pnet_α x)) `` {u} 
                ∧ distinct ((pn_succ (pnet_α x)) u));
              ASSERT(∀u. set ((pn_pred (pnet_α x)) u) = 
                (Graph.E (pn_c (pnet_α x)))¯ `` {u} 
                ∧ distinct ((pn_pred (pnet_α x)) u));
            
              let succ_s = (reachable_impl (graph_of_impl x s));
              let pred_t = (reachable_impl (rev_graph_of_impl x t));
              if (sets_eq_impl (pn_V' x) succ_s) 
                ∧ (sets_eq_impl (pn_V' x) pred_t) 
              then
                RETURN (Some (net_α (pn_c' x, pn_adjmap' x)))
              else
                RETURN None
            }
          else
            RETURN None
        }
      }
    }"     
  
  lemma aux1: "(x', x) ∈ pnet_rel ⟹ (pn_V' x', pn_V x) ∈ br ahs.α ahs.invar"
    unfolding pnet_rel_def br_def pnet_α_def by auto

  lemma [simp]: "graph (graph_of pn s)"
    apply unfold_locales
    unfolding graph_of_def
    by auto

  lemma [simp]: "graph (rev_graph_of pn s)"
    apply unfold_locales
    unfolding rev_graph_of_def
    by auto


  context begin
  private lemma sets_eq_impl_correct_aux1:
    assumes A: "(pn', pn) ∈ pnet_rel"  
    assumes WF: "well_formed_pn pn" 

    assumes F: "finite ((Graph.E (pn_c (pnet_α pn')))⇧* `` {s})"
    shows "sets_eq_impl (pn_V' pn') (reachable_impl (graph_of_impl pn' s))
      ⟷ pn_V pn = (g_E (graph_of pn s))⇧* `` g_V0 (graph_of pn s)"
  proof -
    from A have S1i: "(pn_V' pn', pn_V pn) ∈ br ahs.α ahs.invar"
      unfolding pnet_rel_def br_def pnet_α_def by auto

    note GI = graph_of_impl_correct[OF WF A]
    have G: "graph (graph_of pn s)" by simp

    have F': "finite ((g_E (graph_of pn s))⇧* `` g_V0 (graph_of pn s))"
      using F A by (simp add: graph_of_def pnet_α_def pnet_rel_def br_def)

    note S2i = reachable_impl.refine[simplified, OF F' G GI]  

    from sets_eq_impl.refine[simplified, OF S1i S2i] show ?thesis .
  qed 

  private lemma sets_eq_impl_correct_aux2:
    assumes A: "(pn', pn) ∈ pnet_rel"  
    assumes WF: "rev_well_formed_pn pn" 

    assumes F: "finite (((Graph.E (pn_c (pnet_α pn')))¯)⇧* `` {s})"
    shows "sets_eq_impl (pn_V' pn') (reachable_impl (rev_graph_of_impl pn' s))
      ⟷ pn_V pn = (g_E (rev_graph_of pn s))⇧* `` g_V0 (rev_graph_of pn s)"
  proof -
    from A have S1i: "(pn_V' pn', pn_V pn) ∈ br ahs.α ahs.invar"
      unfolding pnet_rel_def br_def pnet_α_def by auto

    note GI = rev_graph_of_impl_correct[OF WF A]
    have G: "graph (rev_graph_of pn s)" by simp

    have F': "finite ((g_E (rev_graph_of pn s))⇧* `` g_V0 (rev_graph_of pn s))"
      using F A by (simp add: rev_graph_of_def pnet_α_def pnet_rel_def br_def)

    note S2i = reachable_impl.refine[simplified, OF F' G GI]  

    from sets_eq_impl.refine[simplified, OF S1i S2i] show ?thesis .
  qed 



  lemma checkNet3_correct: "checkNet3 el s t ≤ checkNet2 el s t" 
    unfolding checkNet3_def checkNet2_def
    apply (rule refine_IdD)
    apply (refine_rcg)
    apply clarsimp_all
    apply (rule introR[where R="⟨pnet_rel⟩option_rel"])
    apply (simp add: read'_correct_alt; fail)
    apply ((simp add: pnet_rel_def br_def pnet_α_def)+) [7]
    apply (subst sets_eq_impl_correct_aux1; assumption?)
    apply (simp add: well_formed_pn_def)
    
    apply (subst sets_eq_impl_correct_aux2; assumption?)
    apply (simp add: rev_well_formed_pn_def)

    apply simp

    apply (simp add: net_α_def o_def pnet_α_def pnet_rel_def br_def)
    done

  end  


  schematic_goal checkNet4: "RETURN ?c ≤ checkNet3 el s t"
    unfolding checkNet3_def
    by (refine_transfer)
  concrete_definition checkNet4 for el s t uses checkNet4
    

  lemma checkNet4_correct: "case checkNet4 el s t of 
      Some (c, adjmap) ⇒ (el, c) ∈ ln_rel 
        ∧ Network c s t ∧ Graph.is_adj_map c adjmap
    | None ⇒ ¬ln_invar el ∨ ¬Network (ln_α el) s t"
  proof -  
    note checkNet4.refine 
    also note checkNet3_correct 
    also note checkNet2_correct
    also note checkNet_correct
    finally show ?thesis by simp
  qed  

subsection ‹Executable Network Checker›

  definition prepareNet :: "edge_list ⇒ node ⇒ node 
    ⇒ (capacity_impl graph × (node⇒node list) × nat) option"
    ― ‹Read an edge list and a source/sink node, and return a network graph,
      an adjacency map, and the maximum node number plus one. 
      If the edge list or network is invalid, return ‹NONE›.›
  where
    "prepareNet el s t ≡ do {
      (c,adjmap) ← checkNet4 el s t;
      let N = ln_N el;
      Some (c,adjmap,N)
    }"

  export_code prepareNet checking SML  

  theorem prepareNet_correct: "case (prepareNet el s t) of 
      Some (c, adjmap,N) ⇒ (el, c) ∈ ln_rel ∧ Network c s t 
        ∧ Graph.is_adj_map c adjmap ∧ Graph.V c ⊆ {0..<N}
    | None ⇒ ¬ln_invar el ∨ ¬Network (ln_α el) s t"
    using checkNet4_correct[of el s t] ln_N_correct[of el]
    unfolding prepareNet_def
    by (auto split: Option.bind_split simp: ln_rel_def br_def)

end