Theory Graph_Impl

(* TODO: That's quite specific to the BFS alg. Move to Edka! *)
theory Graph_Impl
imports "Lib/Refine_Add_Fofu" Graph
begin

― ‹Fixing capacities to integer values›
type_synonym capacity_impl = int (* TODO: DUP in Network_Impl. Remove here!*)


locale Impl_Succ =
  fixes absG :: "'ga ⇒ capacity_impl graph" 
  fixes ifT :: "'ig itself"
  fixes succ :: "'ga ⇒ node ⇒ node list nres"
  fixes isG :: "'ga ⇒ 'gi ⇒ assn"
  fixes succ_impl :: "'gi ⇒ node ⇒ node list Heap"
  (*assumes [constraint_rules]: "precise isG"*)
  assumes si_rule[sepref_fr_rules]: "(uncurry succ_impl,(uncurry succ)) ∈ [λ(c,u). u∈Graph.V (absG c)]⇩a isG⇧k *⇩a (pure nat_rel)⇧k → list_assn (pure nat_rel)"
begin
  lemma this_loc: "Impl_Succ absG succ isG succ_impl" by unfold_locales

  sepref_register "succ" :: "'ig ⇒ node ⇒ node list nres" (* TODO: Will not work if succ is not a constant! *) 
end


end