Theory CAVA_Automata.Digraph_Impl

section ‹Implementing Graphs›
(* Author: Peter Lammich *)
theory Digraph_Impl
imports Digraph
begin

subsection ‹Directed Graphs by Successor Function›
type_synonym 'a slg = "'a ⇒ 'a list"


definition slg_rel :: "('a×'b) set ⇒ ('a slg × 'b digraph) set" where 
  slg_rel_def_internal: "slg_rel R ≡ 
  (R → ⟨R⟩list_set_rel) O br (λsuccs. {(u,v). v∈succs u}) (λ_. True)"

lemma slg_rel_def: "⟨R⟩slg_rel = 
  (R → ⟨R⟩list_set_rel) O br (λsuccs. {(u,v). v∈succs u}) (λ_. True)"
  unfolding slg_rel_def_internal relAPP_def by simp

lemma slg_rel_sv[relator_props]: 
  "⟦single_valued R; Range R = UNIV⟧ ⟹ single_valued (⟨R⟩slg_rel)"
  unfolding slg_rel_def
  by (tagged_solver)

consts i_slg :: "interface ⇒ interface"
lemmas [autoref_rel_intf] = REL_INTFI[of slg_rel i_slg]

definition [simp]: "op_slg_succs E v ≡ E``{v}"

lemma [autoref_itype]: "op_slg_succs ::i ⟨I⟩ii_slg →i I →i ⟨I⟩ii_set" by simp

context begin interpretation autoref_syn .
lemma [autoref_op_pat]: "E``{v} ≡ op_slg_succs$E$v" by simp
end

lemma refine_slg_succs[autoref_rules_raw]: 
  "(λsuccs v. succs v,op_slg_succs)∈⟨R⟩slg_rel→R→⟨R⟩list_set_rel"
  apply (intro fun_relI)
  apply (auto simp add: slg_rel_def br_def dest: fun_relD)
  done

definition "E_of_succ succ ≡ { (u,v). v∈succ u }"
definition "succ_of_E E ≡ (λu. {v . (u,v)∈E})"

lemma E_of_succ_of_E[simp]: "E_of_succ (succ_of_E E) = E"
  unfolding E_of_succ_def succ_of_E_def
  by auto

lemma succ_of_E_of_succ[simp]: "succ_of_E (E_of_succ E) = E"
  unfolding E_of_succ_def succ_of_E_def
  by auto


context begin interpretation autoref_syn .
  lemma [autoref_itype]: "E_of_succ ::i (I →i ⟨I⟩ii_set) →i ⟨I⟩ii_slg" by simp
  lemma [autoref_itype]: "succ_of_E ::i ⟨I⟩ii_slg →i I →i ⟨I⟩ii_set" by simp
end

lemma E_of_succ_refine[autoref_rules]:
  "(λx. x, E_of_succ) ∈ (R → ⟨R⟩list_set_rel) → ⟨R⟩slg_rel"
  "(λx. x, succ_of_E) ∈ ⟨R⟩slg_rel → (R → ⟨R⟩list_set_rel)"
  unfolding E_of_succ_def[abs_def] succ_of_E_def[abs_def] slg_rel_def br_def
  apply auto []
  apply clarsimp
  apply (blast dest: fun_relD)
  done


subsubsection ‹Restricting Edges›
definition op_graph_restrict :: "'v set ⇒ 'v set ⇒ ('v × 'v) set ⇒ ('v × 'v) set"
  where [simp]: "op_graph_restrict Vl Vr E ≡ E ∩ Vl × Vr"

definition op_graph_restrict_left :: "'v set ⇒ ('v × 'v) set ⇒ ('v × 'v) set"
  where [simp]: "op_graph_restrict_left Vl E ≡ E ∩ Vl × UNIV"

definition op_graph_restrict_right :: "'v set ⇒ ('v × 'v) set ⇒ ('v × 'v) set"
  where [simp]: "op_graph_restrict_right Vr E ≡ E ∩ UNIV × Vr"

lemma [autoref_op_pat]: 
  "E ∩ (Vl × Vr) ≡ op_graph_restrict Vl Vr E"
  "E ∩ (Vl × UNIV) ≡ op_graph_restrict_left Vl E"
  "E ∩ (UNIV × Vr) ≡ op_graph_restrict_right Vr E"
  by simp_all

lemma graph_restrict_aimpl: "op_graph_restrict Vl Vr E = 
  E_of_succ (λv. if v∈Vl then {x ∈ E``{v}. x∈Vr} else {})"
  by (auto simp: E_of_succ_def succ_of_E_def split: if_split_asm)
lemma graph_restrict_left_aimpl: "op_graph_restrict_left Vl E = 
  E_of_succ (λv. if v∈Vl then E``{v} else {})"
  by (auto simp: E_of_succ_def succ_of_E_def split: if_split_asm)
lemma graph_restrict_right_aimpl: "op_graph_restrict_right Vr E = 
  E_of_succ (λv. {x ∈ E``{v}. x∈Vr})"
  by (auto simp: E_of_succ_def succ_of_E_def split: if_split_asm)

schematic_goal graph_restrict_impl_aux:
  fixes Rsl Rsr
  notes [autoref_rel_intf] = REL_INTFI[of Rsl i_set] REL_INTFI[of Rsr i_set]
  assumes [autoref_rules]: "(meml, (∈)) ∈ R → ⟨R⟩Rsl → bool_rel"
  assumes [autoref_rules]: "(memr, (∈)) ∈ R → ⟨R⟩Rsr → bool_rel"
  shows "(?c, op_graph_restrict) ∈ ⟨R⟩Rsl → ⟨R⟩Rsr → ⟨R⟩slg_rel → ⟨R⟩slg_rel"
  unfolding graph_restrict_aimpl[abs_def]
  apply (autoref (keep_goal))
  done

schematic_goal graph_restrict_left_impl_aux:
  fixes Rsl Rsr
  notes [autoref_rel_intf] = REL_INTFI[of Rsl i_set] REL_INTFI[of Rsr i_set]
  assumes [autoref_rules]: "(meml, (∈)) ∈ R → ⟨R⟩Rsl → bool_rel"
  shows "(?c, op_graph_restrict_left) ∈ ⟨R⟩Rsl → ⟨R⟩slg_rel → ⟨R⟩slg_rel"
  unfolding graph_restrict_left_aimpl[abs_def]
  apply (autoref (keep_goal, trace))
  done

schematic_goal graph_restrict_right_impl_aux:
  fixes Rsl Rsr
  notes [autoref_rel_intf] = REL_INTFI[of Rsl i_set] REL_INTFI[of Rsr i_set]
  assumes [autoref_rules]: "(memr, (∈)) ∈ R → ⟨R⟩Rsr → bool_rel"
  shows "(?c, op_graph_restrict_right) ∈ ⟨R⟩Rsr → ⟨R⟩slg_rel → ⟨R⟩slg_rel"
  unfolding graph_restrict_right_aimpl[abs_def]
  apply (autoref (keep_goal, trace))
  done

concrete_definition graph_restrict_impl uses graph_restrict_impl_aux
concrete_definition graph_restrict_left_impl uses graph_restrict_left_impl_aux
concrete_definition graph_restrict_right_impl uses graph_restrict_right_impl_aux

context begin interpretation autoref_syn .
  lemma [autoref_itype]:
    "op_graph_restrict ::i ⟨I⟩ii_set →i ⟨I⟩ii_set →i ⟨I⟩ii_slg →i ⟨I⟩ii_slg"
    "op_graph_restrict_right ::i ⟨I⟩ii_set →i ⟨I⟩ii_slg →i ⟨I⟩ii_slg"
    "op_graph_restrict_left ::i ⟨I⟩ii_set →i ⟨I⟩ii_slg →i ⟨I⟩ii_slg"
    by auto
end

lemmas [autoref_rules_raw] = 
  graph_restrict_impl.refine[OF GEN_OP_D GEN_OP_D]
  graph_restrict_left_impl.refine[OF GEN_OP_D]
  graph_restrict_right_impl.refine[OF GEN_OP_D]

schematic_goal "(?c::?'c, λ(E::nat digraph) x. E``{x}) ∈ ?R"
  apply (autoref (keep_goal))
  done

lemma graph_minus_aimpl: 
  fixes E1 E2 :: "'a rel"
  shows "E1-E2 = E_of_succ (λx. E1``{x} - E2``{x})"
  by (auto simp: E_of_succ_def)

schematic_goal graph_minus_impl_aux:
  fixes R :: "('vi×'v) set"
  assumes [autoref_rules]: "(eq,(=))∈R→R→bool_rel"
  shows "(?c, (-)) ∈ ⟨R⟩slg_rel → ⟨R⟩slg_rel → ⟨R⟩slg_rel"
  apply (subst graph_minus_aimpl[abs_def])
  apply (autoref (keep_goal,trace))
  done

lemmas [autoref_rules] = graph_minus_impl_aux[OF GEN_OP_D]


lemma graph_minus_set_aimpl: 
  fixes E1 E2 :: "'a rel"
  shows "E1-E2 = E_of_succ (λu. {v∈E1``{u}. (u,v)∉E2})"
  by (auto simp: E_of_succ_def)

schematic_goal graph_minus_set_impl_aux:
  fixes R :: "('vi×'v) set"
  assumes [autoref_rules]: "(eq,(=))∈R→R→bool_rel"
  assumes [autoref_rules]: "(mem,(∈)) ∈ R ×r R → ⟨R ×r R⟩Rs → bool_rel"
  shows "(?c, (-)) ∈ ⟨R⟩slg_rel → ⟨R×rR⟩Rs → ⟨R⟩slg_rel"
  apply (subst graph_minus_set_aimpl[abs_def])
  apply (autoref (keep_goal,trace))
  done

lemmas [autoref_rules (overloaded)] = graph_minus_set_impl_aux[OF GEN_OP_D GEN_OP_D]



subsection ‹Rooted Graphs›

subsubsection ‹Operation Identification Setup›

consts
  i_g_ext :: "interface ⇒ interface ⇒ interface"

abbreviation "i_frg ≡ ⟨i_unit⟩ii_g_ext"

context begin interpretation autoref_syn .

lemma g_type[autoref_itype]:
  "g_V ::i ⟨Ie,I⟩ii_g_ext →i ⟨I⟩ii_set"
  "g_E ::i ⟨Ie,I⟩ii_g_ext →i ⟨I⟩ii_slg"
  "g_V0 ::i ⟨Ie,I⟩ii_g_ext →i ⟨I⟩ii_set"
  "graph_rec_ext
    ::i ⟨I⟩ii_set →i ⟨I⟩ii_slg →i ⟨I⟩ii_set →i iE →i ⟨Ie,I⟩ii_g_ext" 
  by simp_all

end


subsubsection ‹Generic Implementation›
record ('vi,'ei,'v0i) gen_g_impl =
  gi_V :: 'vi
  gi_E :: 'ei
  gi_V0 :: 'v0i

definition gen_g_impl_rel_ext_internal_def: "⋀ Rm Rv Re Rv0. gen_g_impl_rel_ext Rm Rv Re Rv0
  ≡ { (gen_g_impl_ext Vi Ei V0i mi, graph_rec_ext V E V0 m) 
      | Vi Ei V0i mi V E V0 m. 
        (Vi,V)∈Rv ∧ (Ei,E)∈Re ∧ (V0i,V0)∈Rv0 ∧ (mi,m)∈Rm
    }"

lemma gen_g_impl_rel_ext_def: "⋀Rm Rv Re Rv0. ⟨Rm,Rv,Re,Rv0⟩gen_g_impl_rel_ext
  ≡ { (gen_g_impl_ext Vi Ei V0i mi, graph_rec_ext V E V0 m) 
      | Vi Ei V0i mi V E V0 m. 
        (Vi,V)∈Rv ∧ (Ei,E)∈Re ∧ (V0i,V0)∈Rv0 ∧ (mi,m)∈Rm
    }"
  unfolding gen_g_impl_rel_ext_internal_def relAPP_def by simp

lemma gen_g_impl_rel_sv[relator_props]: 
  "⋀Rm Rv Re Rv0. ⟦single_valued Rv; single_valued Re; single_valued Rv0; single_valued Rm ⟧ ⟹ 
  single_valued (⟨Rm,Rv,Re,Rv0⟩gen_g_impl_rel_ext)"
  unfolding gen_g_impl_rel_ext_def
  apply (auto 
    intro!: single_valuedI 
    dest: single_valuedD slg_rel_sv list_set_rel_sv)
  done

lemma gen_g_refine:
  "⋀Rm Rv Re Rv0. (gi_V,g_V) ∈ ⟨Rm,Rv,Re,Rv0⟩gen_g_impl_rel_ext → Rv"
  "⋀Rm Rv Re Rv0. (gi_E,g_E) ∈ ⟨Rm,Rv,Re,Rv0⟩gen_g_impl_rel_ext → Re"
  "⋀Rm Rv Re Rv0. (gi_V0,g_V0) ∈ ⟨Rm,Rv,Re,Rv0⟩gen_g_impl_rel_ext → Rv0"
  "⋀Rm Rv Re Rv0. (gen_g_impl_ext, graph_rec_ext) 
    ∈ Rv → Re → Rv0 → Rm → ⟨Rm,Rv,Re,Rv0⟩gen_g_impl_rel_ext"
  unfolding gen_g_impl_rel_ext_def
  by auto

subsubsection ‹Implementation with list-set for Nodes›
type_synonym ('v,'m) frgv_impl_scheme = 
  "('v list, 'v ⇒ 'v list, 'v list, 'm) gen_g_impl_scheme"

definition frgv_impl_rel_ext_internal_def: 
  "frgv_impl_rel_ext Rm Rv 
  ≡ ⟨Rm,⟨Rv⟩list_set_rel,⟨Rv⟩slg_rel,⟨Rv⟩list_set_rel⟩gen_g_impl_rel_ext"

lemma frgv_impl_rel_ext_def: "⟨Rm,Rv⟩frgv_impl_rel_ext
  ≡ ⟨Rm,⟨Rv⟩list_set_rel,⟨Rv⟩slg_rel,⟨Rv⟩list_set_rel⟩gen_g_impl_rel_ext"
  unfolding frgv_impl_rel_ext_internal_def relAPP_def by simp

lemma [autoref_rel_intf]: "REL_INTF frgv_impl_rel_ext i_g_ext"
  by (rule REL_INTFI)

lemma [relator_props, simp]: 
  "⟦single_valued Rv; Range Rv = UNIV; single_valued Rm⟧ 
  ⟹ single_valued (⟨Rm,Rv⟩frgv_impl_rel_ext)"
  unfolding frgv_impl_rel_ext_def by tagged_solver

lemmas [param, autoref_rules] = gen_g_refine[where 
  Rv = "⟨Rv⟩list_set_rel" and Re = "⟨Rv⟩slg_rel" and ?Rv0.0 = "⟨Rv⟩list_set_rel"
  for Rv, folded frgv_impl_rel_ext_def]

subsubsection ‹Implementation with Cfun for Nodes›
text ‹This implementation allows for the universal node set.›
type_synonym ('v,'m) g_impl_scheme = 
  "('v ⇒ bool, 'v ⇒ 'v list, 'v list, 'm) gen_g_impl_scheme"

definition g_impl_rel_ext_internal_def: 
  "g_impl_rel_ext Rm Rv 
  ≡ ⟨Rm,⟨Rv⟩fun_set_rel,⟨Rv⟩slg_rel,⟨Rv⟩list_set_rel⟩gen_g_impl_rel_ext"

lemma g_impl_rel_ext_def: "⟨Rm,Rv⟩g_impl_rel_ext
  ≡ ⟨Rm,⟨Rv⟩fun_set_rel,⟨Rv⟩slg_rel,⟨Rv⟩list_set_rel⟩gen_g_impl_rel_ext"
  unfolding g_impl_rel_ext_internal_def relAPP_def by simp

lemma [autoref_rel_intf]: "REL_INTF g_impl_rel_ext i_g_ext"
  by (rule REL_INTFI)

lemma [relator_props, simp]: 
  "⟦single_valued Rv; Range Rv = UNIV; single_valued Rm⟧ 
  ⟹ single_valued (⟨Rm,Rv⟩g_impl_rel_ext)"
  unfolding g_impl_rel_ext_def by tagged_solver

lemmas [param, autoref_rules] = gen_g_refine[where 
  Rv = "⟨Rv⟩fun_set_rel" 
  and Re = "⟨Rv⟩slg_rel" 
  and ?Rv0.0 = "⟨Rv⟩list_set_rel" 
  for Rv, folded g_impl_rel_ext_def]

lemma [autoref_rules]: "(gi_V_update, g_V_update) ∈ (⟨Rv⟩fun_set_rel → ⟨Rv⟩fun_set_rel) →
  ⟨Rm, Rv⟩g_impl_rel_ext → ⟨Rm, Rv⟩g_impl_rel_ext"
  unfolding g_impl_rel_ext_def gen_g_impl_rel_ext_def
  by (auto, metis (full_types) tagged_fun_relD_both)
lemma [autoref_rules]: "(gi_E_update, g_E_update) ∈ (⟨Rv⟩slg_rel → ⟨Rv⟩slg_rel) →
  ⟨Rm, Rv⟩g_impl_rel_ext → ⟨Rm, Rv⟩g_impl_rel_ext"
  unfolding g_impl_rel_ext_def gen_g_impl_rel_ext_def
  by (auto, metis (full_types) tagged_fun_relD_both)
lemma [autoref_rules]: "(gi_V0_update, g_V0_update) ∈ (⟨Rv⟩list_set_rel → ⟨Rv⟩list_set_rel) →
  ⟨Rm, Rv⟩g_impl_rel_ext → ⟨Rm, Rv⟩g_impl_rel_ext"
  unfolding g_impl_rel_ext_def gen_g_impl_rel_ext_def
  by (auto, metis (full_types) tagged_fun_relD_both)

(* HACK: The homgeneity rule heuristics erronously creates a homogeneity rule that
    equalizes Rv and Rv0, out of the frv-implementation, which happens to be the
    first. This declaration counters the undesired effects caused by this. *)
lemma [autoref_hom]: 
  "CONSTRAINT graph_rec_ext (⟨Rv⟩Rvs → ⟨Rv⟩Res → ⟨Rv⟩Rv0s → Rm → ⟨Rm,Rv⟩Rg)"
  by simp


schematic_goal "(?c::?'c, λG x. g_E G `` {x})∈?R"
  apply (autoref (keep_goal))
  done

schematic_goal "(?c,λV0 E.
   ⦇ g_V = UNIV, g_E = E, g_V0 = V0 ⦈  )
  ∈⟨R⟩list_set_rel → ⟨R⟩slg_rel → ⟨unit_rel,R⟩g_impl_rel_ext"
  apply (autoref (keep_goal))
  done

schematic_goal "(?c,λV V0 E.
   ⦇ g_V = V, g_E = E, g_V0 = V0 ⦈  )
  ∈⟨R⟩list_set_rel → ⟨R⟩list_set_rel → ⟨R⟩slg_rel → ⟨unit_rel,R⟩frgv_impl_rel_ext"
  apply (autoref (keep_goal))
  done

subsubsection ‹Renaming›

definition "the_inv_into_map V f x 
  = (if x ∈ f`V then Some (the_inv_into V f x) else None)"

lemma the_inv_into_map_None[simp]:
  "the_inv_into_map V f x = None ⟷ x ∉ f`V"
  unfolding the_inv_into_map_def by auto

lemma the_inv_into_map_Some':
  "the_inv_into_map V f x = Some y ⟷ x ∈ f`V ∧ y=the_inv_into V f x"
  unfolding the_inv_into_map_def by auto

lemma the_inv_into_map_Some[simp]:
  "inj_on f V ⟹ the_inv_into_map V f x = Some y ⟷ y∈V ∧ x=f y"
  by (auto simp: the_inv_into_map_Some' the_inv_into_f_f)

definition "the_inv_into_map_impl V f = 
  FOREACH V (λx m. RETURN (m(f x ↦ x))) Map.empty"

lemma the_inv_into_map_impl_correct:
  assumes [simp]: "finite V"
  assumes INJ: "inj_on f V"
  shows "the_inv_into_map_impl V f ≤ SPEC (λr. r = the_inv_into_map V f)"
  unfolding the_inv_into_map_impl_def
  apply (refine_rcg 
    FOREACH_rule[where I="λit m. m=the_inv_into_map (V - it) f"]
    refine_vcg
  )

  apply (vc_solve 
    simp: the_inv_into_map_def[abs_def] it_step_insert_iff 
    intro!: ext)

  apply (intro allI impI conjI)

  apply (subst the_inv_into_f_f[OF subset_inj_on[OF INJ]], auto) []

  apply (subst the_inv_into_f_f[OF subset_inj_on[OF INJ]], auto) []

  apply safe []
  apply (subst the_inv_into_f_f[OF subset_inj_on[OF INJ]], (auto) [2])+
  apply simp
  done

schematic_goal the_inv_into_map_code_aux:
  fixes Rv' :: "('vti × 'vt) set"
  assumes [autoref_ga_rules]: "is_bounded_hashcode Rv' eq bhc"
  assumes [autoref_ga_rules]: "is_valid_def_hm_size TYPE('vti) (def_size)"
  assumes [autoref_rules]: "(Vi,V)∈⟨Rv⟩list_set_rel"
  assumes [autoref_rules]: "(fi,f)∈Rv→Rv'"
  shows "(RETURN ?c, the_inv_into_map_impl V f) ∈ ⟨⟨Rv',Rv⟩ahm_rel bhc⟩nres_rel"
  unfolding the_inv_into_map_impl_def[abs_def]
  apply (autoref_monadic (plain))
  done

concrete_definition the_inv_into_map_code uses the_inv_into_map_code_aux
export_code the_inv_into_map_code checking SML

thm the_inv_into_map_code.refine

context begin interpretation autoref_syn .
lemma autoref_the_inv_into_map[autoref_rules]:
  fixes Rv' :: "('vti × 'vt) set"
  assumes "SIDE_GEN_ALGO (is_bounded_hashcode Rv' eq bhc)"
  assumes "SIDE_GEN_ALGO (is_valid_def_hm_size TYPE('vti) def_size)"
  assumes INJ: "SIDE_PRECOND (inj_on f V)"
  assumes V: "(Vi,V)∈⟨Rv⟩list_set_rel"
  assumes F: "(fi,f)∈Rv→Rv'"
  shows "(the_inv_into_map_code eq bhc def_size Vi fi, 
    (OP the_inv_into_map 
      ::: ⟨Rv⟩list_set_rel → (Rv→Rv') → ⟨Rv', Rv⟩Impl_Array_Hash_Map.ahm_rel bhc)
    $V$f) ∈ ⟨Rv', Rv⟩Impl_Array_Hash_Map.ahm_rel bhc"
proof simp

  from V have FIN: "finite V" using list_set_rel_range by auto

  note the_inv_into_map_code.refine[
    OF assms(1-2,4-5)[unfolded autoref_tag_defs], THEN nres_relD 
  ]
  also note the_inv_into_map_impl_correct[OF FIN INJ[unfolded autoref_tag_defs]]
  finally show "(the_inv_into_map_code eq bhc def_size Vi fi, the_inv_into_map V f)
    ∈ ⟨Rv', Rv⟩Impl_Array_Hash_Map.ahm_rel bhc"
    by (simp add: refine_pw_simps pw_le_iff)
qed

end

schematic_goal "(?c::?'c, do { 
  let s = {1,2,3::nat}; 
  ⌦‹ASSERT (inj_on Suc s);›
  RETURN (the_inv_into_map s Suc) }) ∈ ?R"
  apply (autoref (keep_goal))
  done


definition "fr_rename_ext_aimpl ecnv f G ≡ do {
    ASSERT (inj_on f (g_V G));
    ASSERT (inj_on f (g_V0 G));
    let fi_map = the_inv_into_map (g_V G) f;
    e ← ecnv fi_map G;
    RETURN ⦇
      g_V = f`(g_V G),
      g_E = (E_of_succ (λv. case fi_map v of
          Some u ⇒ f ` (succ_of_E (g_E G) u) | None ⇒ {})),
      g_V0 = (f`g_V0 G),
      … = e
    ⦈
  }"

context g_rename_precond begin

  definition "fi_map x = (if x ∈ f`V then Some (fi x) else None)"
  lemma fi_map_alt: "fi_map = the_inv_into_map V f"
    apply (rule ext)
    unfolding fi_map_def the_inv_into_map_def fi_def
    by simp
    
  lemma fi_map_Some: "(fi_map u = Some v) ⟷ u∈f`V ∧ fi u = v"
    unfolding fi_map_def by (auto split: if_split_asm)

  lemma fi_map_None: "(fi_map u = None) ⟷ u∉f`V"
    unfolding fi_map_def by (auto split: if_split_asm)

  lemma rename_E_aimpl_alt: "rename_E f E = E_of_succ (λv. case fi_map v of
    Some u ⇒ f ` (succ_of_E E u) | None ⇒ {})"
    unfolding E_of_succ_def succ_of_E_def
    using E_ss
    by (force 
      simp: fi_f f_fi fi_map_Some fi_map_None 
      split: if_split_asm option.splits)


  lemma frv_rename_ext_aimpl_alt: 
    assumes ECNV: "ecnv' fi_map G ≤ SPEC (λr. r = ecnv G)"
    shows "fr_rename_ext_aimpl ecnv' f G 
      ≤ SPEC (λr. r = fr_rename_ext ecnv f G)"
  proof -
    (*have [simp]: "⦇ g_E =
             E_of_succ
              (λv. case the_inv_into_map V f v of None ⇒ {}
                 | Some u ⇒ f ` succ_of_E (g_E G) u),
            g_V0 = f ` g_V0 G, … = ecnv Gv⦈
      = frv_G (frv_rename_ext ecnv f Gv)"
      unfolding frv_rename_ext_def 
      by (auto simp: rename_E_aimpl_alt fi_map_alt)

    have [simp]: "⦇frv_V = f ` V, frv_G = frv_G Gv'⦈ = Gv'"
      unfolding frv_rename_ext_def
      by simp*)

    show ?thesis
      unfolding fr_rename_ext_def fr_rename_ext_aimpl_def
      apply (refine_rcg 
        order_trans[OF ECNV[unfolded fi_map_alt]] 
        refine_vcg)
      using subset_inj_on[OF _ V0_ss]
      apply (auto intro: INJ simp: rename_E_aimpl_alt fi_map_alt)
      done
  qed
end

term frv_rename_ext_aimpl
schematic_goal fr_rename_ext_impl_aux:
  fixes Re and Rv' :: "('vti × 'vt) set"
  assumes [autoref_rules]: "(eq, (=)) ∈ Rv' → Rv' → bool_rel"
  assumes [autoref_ga_rules]: "is_bounded_hashcode Rv' eq bhc"
  assumes [autoref_ga_rules]: "is_valid_def_hm_size TYPE('vti) def_size"
  shows "(?c,fr_rename_ext_aimpl) ∈ 
    ((⟨Rv',Rv⟩ahm_rel bhc) → ⟨Re,Rv⟩frgv_impl_rel_ext → ⟨Re'⟩nres_rel) →   
    (Rv→Rv') →
    ⟨Re,Rv⟩frgv_impl_rel_ext → 
    ⟨⟨Re',Rv'⟩frgv_impl_rel_ext⟩nres_rel"
  unfolding fr_rename_ext_aimpl_def[abs_def]
  apply (autoref (keep_goal))
  done

concrete_definition fr_rename_ext_impl uses fr_rename_ext_impl_aux

thm fr_rename_ext_impl.refine[OF GEN_OP_D SIDE_GEN_ALGO_D SIDE_GEN_ALGO_D]

subsection ‹Graphs from Lists›

definition succ_of_list :: "(nat×nat) list ⇒ nat ⇒ nat set"
  where
  "succ_of_list l ≡ let
    m = fold (λ(u,v) g. 
          case g u of 
            None ⇒ g(u↦{v})
          | Some s ⇒ g(u↦insert v s)
        ) l Map.empty
  in
    (λu. case m u of None ⇒ {} | Some s ⇒ s)"
    
lemma succ_of_list_correct_aux: 
  "(succ_of_list l, set l) ∈ br (λsuccs. {(u,v). v∈succs u}) (λ_. True)"
proof -

  term the_default

  { fix m
    have "fold (λ(u,v) g. 
            case g u of 
              None ⇒ g(u↦{v})
            | Some s ⇒ g(u↦insert v s)
          ) l m 
      = (λu. let s=set l `` {u} in 
          if s={} then m u else Some (the_default {} (m u) ∪ s))"
      apply (induction l arbitrary: m)
      apply (auto 
        split: option.split if_split 
        simp: Let_def Image_def
        intro!: ext)
      done
  } note aux=this
  
  show ?thesis
    unfolding succ_of_list_def aux
    by (auto simp: br_def Let_def split: option.splits if_split_asm)
qed


schematic_goal succ_of_list_impl:
  notes [autoref_tyrel] = 
    ty_REL[where 'a="nat⇀nat set" and R="⟨nat_rel,R⟩iam_map_rel" for R]
    ty_REL[where 'a="nat set" and R="⟨nat_rel⟩list_set_rel"]

  shows "(?f::?'c,succ_of_list) ∈ ?R"
  unfolding succ_of_list_def[abs_def]
  apply (autoref (keep_goal))
  done

concrete_definition succ_of_list_impl uses succ_of_list_impl
export_code succ_of_list_impl in SML

lemma succ_of_list_impl_correct: "(succ_of_list_impl,set) ∈ Id → ⟨Id⟩slg_rel"
  apply rule
  unfolding slg_rel_def
  apply rule
  apply (rule succ_of_list_impl.refine[THEN fun_relD])
  apply simp
  apply (rule succ_of_list_correct_aux)
  done

end