Theory Graph_Impl

theory Graph_Impl
imports Refine_Add_Fofu Graph
begin

-- ‹Fixing capacities to integer values›
type_synonym capacity_impl = int


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 -> hn_list_aux (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