Theory FordFulkerson_Algo

section ‹The Ford-Fulkerson Method›
theory FordFulkerson_Algo
imports 
  Ford_Fulkerson
  Refine_Add_Fofu
  Refine_Monadic_Syntax_Sugar
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);
    selectp p. NFlow.isAugmentingPath c s t f 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. ¬NFlow.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);

  (f,_) \<leftarrow> while⇗fofu_invar⇖
    (λ(f,brk). ¬brk) 
    (λ(f,_). do {
      p \<leftarrow> find_augmenting_spec f;
      case p of 
        None => return (f,True)
      | Some p => do {
          assert (p≠[]);
          assert (NFlow.isAugmentingPath c s t f p);
          let f' = NFlow.augmentingFlow c f p;
          let f = NFlow.augment c f f';
          assert (NFlow c s t f);
          return (f, False)
        }  
    })
    (f,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)" 
  unfolding NFlow_def Flow_def 
  using Network_axioms
  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 -
  note augment_flow_presv[OF augFlow_resFlow[OF AUG]]
  thus ?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])
  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›

(* TODO: May be a good idea for main refinement branch, too! *)
definition (in NFlow) "augment_with_path p ≡ augment (augmentingFlow p)"

context begin

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

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

  (f,brk) \<leftarrow> while (λ(f,brk). ¬brk) 
    (λ(f,brk). do {
      p \<leftarrow> selectp p. is_augmenting_path f p;
      case p of 
        None => return (f,True)
      | Some p => return (augment c f p, False)
    })
    (f,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)
    done
  also note fofu_partial_correct  
  finally show ?thesis .
qed  

end -- ‹Theory›