Theory FordFulkerson_Algo

section ‹The Ford-Fulkerson Method›
theory FordFulkerson_Algo
imports 
  Flow_Networks.Ford_Fulkerson
  Flow_Networks.Refine_Add_Fofu
begin
text ‹In this theory, we formalize the abstract Ford-Fulkerson
  method, which is independent of how an augmenting path is chosen›

context Network 
begin

subsection ‹Algorithm›
text ‹
  We abstractly specify the procedure for finding an augmenting path:
  Assuming a valid flow, the procedure must return an augmenting path 
  iff there exists one.
  ›
definition "find_augmenting_spec f ≡ do {
    assert (NFlow c s t f);
    select p. NPreflow.isAugmentingPath c s t f p
  }"

text ‹Moreover, we specify augmentation of a flow along a path›
definition (in NFlow) "augment_with_path p ≡ augment (augmentingFlow p)"

text ‹
  We also specify the loop invariant, and annotate it to the loop.
›
abbreviation "fofu_invar ≡ λ(f,brk). 
        NFlow c s t f 
      ∧ (brk ⟶ (∀p. ¬NPreflow.isAugmentingPath c s t f p))
    "  

text ‹Finally, we obtain the Ford-Fulkerson algorithm.
  Note that we annotate some assertions to ease later refinement›
definition "fofu ≡ do {
  let f⇩0 = (λ_. 0);

  (f,_) ← while⇗fofu_invar⇖
    (λ(f,brk). ¬brk) 
    (λ(f,_). do {
      p ← find_augmenting_spec f;
      case p of 
        None ⇒ return (f,True)
      | Some p ⇒ do {
          assert (p≠[]);
          assert (NPreflow.isAugmentingPath c s t f p);
          let f = NFlow.augment_with_path c f p;
          assert (NFlow c s t f);
          return (f, False)
        }  
    })
    (f⇩0,False);
  assert (NFlow c s t f);
  return f 
}"

subsection ‹Partial Correctness›
text ‹Correctness of the algorithm is a consequence from the 
  Ford-Fulkerson theorem. We need a few straightforward 
  auxiliary lemmas, though:
›

text ‹The zero flow is a valid flow›
lemma zero_flow: "NFlow c s t (λ_. 0)" 
  apply unfold_locales
  by (auto simp: s_node t_node cap_non_negative)  

text ‹Augmentation preserves the flow property›
lemma (in NFlow) augment_pres_nflow:
  assumes AUG: "isAugmentingPath p"
  shows "NFlow c s t (augment (augmentingFlow p))"
proof -
  from augment_flow_presv[OF augFlow_resFlow[OF AUG]]
  interpret f': Flow c s t "augment (augmentingFlow p)" .
  show ?thesis by intro_locales
qed    

text ‹Augmenting paths cannot be empty›
lemma (in NFlow) augmenting_path_not_empty:
  "¬isAugmentingPath []"
  unfolding isAugmentingPath_def using s_not_t by auto


text ‹Finally, we can use the verification condition generator to
  show correctness›
theorem fofu_partial_correct: "fofu ≤ (spec f. isMaxFlow f)"
  unfolding fofu_def find_augmenting_spec_def 
  apply (refine_vcg)
  apply (vc_solve simp: 
    zero_flow 
    NFlow.augment_pres_nflow 
    NFlow.augmenting_path_not_empty
    NFlow.noAugPath_iff_maxFlow[symmetric]
    NFlow.augment_with_path_def
  )
  done

subsection ‹Algorithm without Assertions›
text ‹For presentation purposes, we extract a version of the algorithm
  without assertions, and using a bit more concise notation›

context begin

private abbreviation (input) "augment 
  ≡ NFlow.augment_with_path"
private abbreviation (input) "is_augmenting_path f p 
  ≡ NPreflow.isAugmentingPath c s t f p"

text ‹ {} ›
text_raw ‹\DefineSnippet{ford_fulkerson_algo}{›       
definition "ford_fulkerson_method ≡ do {
  let f⇩0 = (λ(u,v). 0);

  (f,brk) ← while (λ(f,brk). ¬brk) 
    (λ(f,brk). do {
      p ← select p. is_augmenting_path f p;
      case p of 
        None ⇒ return (f,True)
      | Some p ⇒ return (augment c f p, False)
    })
    (f⇩0,False);
  return f 
}"
text_raw ‹}%EndSnippet›

text ‹ {} ›

end ― ‹Anonymous context› 
end ― ‹Network› 

text ‹ {} ›
text_raw ‹\DefineSnippet{ford_fulkerson_correct}{›       
theorem (in Network) "ford_fulkerson_method ≤ (spec f. isMaxFlow f)"
text_raw ‹}%EndSnippet›
text ‹ {} ›
proof -
  have [simp]: "(λ(u,v). 0) = (λ_. 0)" by auto
  have "ford_fulkerson_method ≤ fofu"
    unfolding ford_fulkerson_method_def fofu_def Let_def find_augmenting_spec_def
    apply (rule refine_IdD)
    apply (refine_vcg)
    apply (refine_dref_type)
    apply (vc_solve simp: NFlow.augment_with_path_def solve: exI)
    done
  also note fofu_partial_correct  
  finally show ?thesis .
qed  

end ― ‹Theory›