Theory FordFulkerson_Algo

section ‹The Ford-Fulkerson Method›
theory FordFulkerson_Algo
imports 
  Flow_Networks.Ford_Fulkerson EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract
 (*  Maxflow_Lib.Refine_Add_Fofu *)
  "../../Refine_Imperative_HOL/Sepref"
  "../../RefineMonadicVCG"
begin
 
text ‹In this theory, we formalize the abstract Ford-Fulkerson
  method, which is independent of how an augmenting path is chosen›


text ‹We specify augmentation of a flow along a path›
definition (in NFlow) "augment_with_path p ≡ augment (augmentingFlow p)"
 
locale FoFu = Network c s t for c :: "'capacity::linordered_idom graph" and s t +
  fixes  R :: "(nat × nat ⇒ 'capacity) ⇒ nat"
     and find_augmenting_time :: "nat "
     and augment_with_path_time :: "nat"
     and init_graph :: "nat ⇒ nat"
     and special_info :: "(nat × nat ⇒ 'capacity) ⇒ (nat × nat) list ⇒ bool"
   assumes ff: "NFlow c s t a ⟹
 ∀x. ¬ special_info a x
   ⟹ NPreflow.isAugmentingPath c s t a x ⟹ False"  

  and R_decreases: "NFlow c s t a ⟹ special_info a x ⟹ R (NFlow.augment_with_path c a x) < R a"

  and fat_g_0[simp]: "⋀x. enat find_augmenting_time ≠ 0"

  and augments: "⋀p f.  NFlow c s t f ⟹ special_info f p ⟹ NPreflow.isAugmentingPath c s t f p"


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 (in FoFu) "find_augmenting_spec f ≡ do {
    ASSERT (NFlow c s t f);
    SELECT (%p. (* NPreflow.isAugmentingPath c s t f p ∧ *) special_info f p) (find_augmenting_time)
  }"


    

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))
    "  

fun (in FoFu) Te where "Te (f,brk) = (if brk then 0 else (find_augmenting_time + augment_with_path_time)  * (1+ R f))"

text ‹Finally, we obtain the Ford-Fulkerson algorithm.
  Note that we annotate some assertions to ease later refinement›
definition (in FoFu) "fofu ≡ do {
  f⇩0 ← SPECT [(λ_. 0) ↦ init_graph (card V)];

  (f,_) ← whileIET fofu_invar Te
    (λ(f,brk). ¬brk) 
    (λ(f,_). do {
      p ← find_augmenting_spec f;
      case p of 
        None ⇒ RETURNT (f,True)
      | Some p ⇒ do {
          ASSERT (p≠[]);
          ASSERT (NPreflow.isAugmentingPath c s t f p);
          f ← SPECT [NFlow.augment_with_path c f p ↦ augment_with_path_time];
          ASSERT (NFlow c s t f);
          RETURNT (f, False)
        }  
    })
    (f⇩0,False);
  ASSERT (NFlow c s t f);
  RETURNT 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›


definition (in FoFu) "maxFlow_time = enat ( init_graph (card V) + (find_augmenting_time + augment_with_path_time) * (R (λ_. 0) + 1)) "


theorem (in FoFu)  fofu_partial_correct: "fofu ≤ SPECT (emb (λf. isMaxFlow f) (maxFlow_time))"
  unfolding fofu_def find_augmenting_spec_def 
  apply(rule T_specifies_I)
  apply(vcg'‹-›)  apply (simp_all)
  subgoal by (auto simp: zero_flow)
  subgoal  using ff by blast
  subgoal apply auto  
    subgoal unfolding NFlow.augment_with_path_def
      using  NFlow.augment_pres_nflow augments by metis
    subgoal 
      apply (auto simp add: Some_le_mm3_Some_conv R_decreases  less_imp_le_nat)  
      by (metis R_decreases diff_mult_distrib2 prod_ineqs2 zero_less_diff)
    done
  subgoal  unfolding NFlow.augment_with_path_def
      using  NFlow.augment_pres_nflow augments by metis  
  subgoal using augments by simp  
  subgoal  using NFlow.augmenting_path_not_empty augments by blast 
  subgoal unfolding maxFlow_time_def apply (auto simp: Some_le_emb'_conv)
    using NFlow.noAugPath_iff_maxFlow[symmetric] by blast 
  done

theorem (in FoFu)  fofu_partial_correct': "fofu ≤ SPECT (emb (λf. isMaxFlow f) (maxFlow_time))"
  unfolding fofu_def find_augmenting_spec_def 
  apply(labeled_VCG) using [[goals_limit = 16]]
  apply (casify) oops

 
(*
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›